Return
Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems
DOI:10.1109/TAC.2020.3010490.png)
Abstract
En 中文
Discrete-time stochastic systems are an essential modeling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis of control strategies are computationally hard and generally rely on the use of approximate abstractions. Building on approximate abstractions, we compute control strategies with lower- and upper-bounds for satisfying unbounded temporal logic specifications. First, robust dynamic programming mappings over the abstract system are introduced to solve the control synthesis and verification problem. These mappings yield a control strategy and a unique lower bound on the satisfaction probability for temporal logic specifications that is robust to the incurred approximation errors. Second, upper-bounds on the satisfaction probability are quantified, and properties of the mappings are analyzed and discussed. Finally, we show the implications of these results to continuous state space of linear stochastic dynamic systems. This abstraction-based synthesis framework is shown to be able to handle infinite-horizon properties. Approximation errors expressed as deviations in the outputs of the models and as deviations in the probabilistic transitions are allowed and are quantified using approximate stochastic simulation relations.
Keywords:
Aerospace electronics
Computational modeling
Markov processes
Robustness
Dynamic programming
Stochastic systems
Approximate simulation relations
control synthesis
temporal logic properties
lifting
robust satisfaction
syntactically co-safe linear temporal logic (scLTL)
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
7
Papers:
1.3W
Citations:
6.7W

