Formal Synthesis of Stochastic Systems via Control Barrier Certificates

被引:68
作者
Jagtap, Pushpak [1 ]
Soudjani, Sadegh [2 ]
Zamani, Majid [3 ,4 ]
机构
[1] Tech Univ Munich, Dept Elect & Comp Engn, D-80333 Munich, Germany
[2] Newcastle Univ, Sch Comp, Newcastle Upon Tyne NE1 7RU, Tyne & Wear, England
[3] Univ Colorado, Dept Comp Sci, Boulder, CO 80309 USA
[4] Ludwig Maximilian Univ Munich, Dept Comp Sci, D-80333 Munich, Germany
基金
欧盟地平线“2020”;
关键词
Stochastic systems; Control systems; Automata; Stochastic processes; Task analysis; Systematics; Uncertainty; Barrier certificates; formal synthesis; linear temporal logic (LTL); stochastic systems; OMEGA-AUTOMATA; VERIFICATION; SAFETY; CONSTRAINTS; FRAMEWORK;
D O I
10.1109/TAC.2020.3013916
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
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.
引用
收藏
页码:3097 / 3110
页数:14
相关论文
共 56 条
[1]   Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems [J].
Abate, Alessandro ;
Prandini, Maria ;
Lygeros, John ;
Sastry, Shankar .
AUTOMATICA, 2008, 44 (11) :2724-2734
[2]  
Althoff M, 2017, IEEE INT VEH SYM, P719, DOI 10.1109/IVS.2017.7995802
[3]   Control Barrier Function Based Quadratic Programs for Safety Critical Systems [J].
Ames, Aaron D. ;
Xu, Xiangru ;
Grizzle, Jessy W. ;
Tabuada, Paulo .
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (08) :3861-3876
[4]  
[Anonymous], 2009, Verification and Control of Hybrid Systems: A Symbolic Approach
[5]  
[Anonymous], 2007, IFAC P
[6]  
Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[7]  
Belta C, 2017, STUD SYST DECIS CONT, V89, P1, DOI 10.1007/978-3-319-50763-7
[8]  
Bertsekas D., 1996, Stochastic Optimal Control: The Discrete-Time Case, V5
[9]  
Bisoffi A, 2018, P AMER CONTR CONF, P634, DOI 10.23919/ACC.2018.8430795
[10]  
De Giacomo G, 2015, PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), P1558