Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems

• 成果类型: Article
• 署名作者: Haesaert, Sofie; Soudjani, Sadegh
• 署名单位: Eindhoven University of Technology; Newcastle University - UK
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2020.3010490
• 发表日期: 2021
• 页码: 2496-2511
• 关键词: 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)

摘要

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.