Formal Synthesis of Stochastic Systems via Control Barrier Certificates

• 成果类型: Article
• 署名作者: Jagtap, Pushpak; Soudjani, Sadegh; Zamani, Majid
• 署名单位: Technical University of Munich; Newcastle University - UK; University of Colorado System; University of Colorado Boulder; University of Munich
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2020.3013916
• 发表日期: 2021
• 页码: 3097-3110
• 关键词: stochastic systems; control systems; Automata; Stochastic processes; Task analysis; systematics; uncertainty; Barrier certificates; formal synthesis; linear temporal logic (LTL); Stochastic systems

摘要

This article focuses on synthesizing control policies for discrete-time stochastic control systems together with a lower bound on the probability that the systems satisfy the complex temporal properties. The desired properties of the system are expressed as linear temporal logic specifications over finite traces. In particular, our approach decomposes the given specification into simpler reachability tasks based on its automata representation. We, then, propose the use of so-called control barrier certificate to solve those simpler reachability tasks along with computing the corresponding controllers and probability bounds. Finally, we combine those controllers to obtain a hybrid control policy solving the considered problem. Under some assumptions, we also provide two systematic approaches for uncountable and finite input sets to search for control barrier certificates. We demonstrate the effectiveness of the proposed approach on a room temperature control and lane keeping of a vehicle modeled as a four-dimensional single-track kinematic model. We compare our results with the discretization-based methods in the literature.