A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems

被引:17
|
作者
Yang, Zhengfeng [1 ]
Huang, Chao [2 ]
Chen, Xin [2 ]
Lin, Wang [3 ]
Liu, Zhiming [4 ]
机构
[1] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China
[2] Nanjing Univ, State Key Lab Novel Software Technol, Nanjing, Jiangsu, Peoples R China
[3] Chinese Acad Sci, AMSS, Key Lab Math Mech, Beijing, Peoples R China
[4] Southwest Univ, Ctr Res & Innovat Software Engn, Chongqing, Peoples R China
来源
FM 2016: FORMAL METHODS | 2016年 / 9995卷
关键词
Formal verification; Hybrid systems; Barrier certificates; Linear programming relaxation; SAFETY VERIFICATION; COMPUTATION;
D O I
10.1007/978-3-319-48989-6_44
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper presents a linear programming (LP) relaxation based approach for generating polynomial barrier certificates for safety verification of semi-algebraic hybrid systems. The key idea is to introduce an LP relaxation to encode the set of nonnegativity constraints derived from the conditions of the associated barrier certificates and then resort to LP solvers to find the solutions. The most important benefit of the LP relaxation based approach is that it possesses a much lower computational complexity and hence can be solved very efficiently, which is demonstrated by the theoretical analysis on complexity as well as the experiment on a set of examples gathered from the literature. As far as we know, it is the first method that enables LP relaxation based polynomial barrier certificate generation.
引用
收藏
页码:721 / 738
页数:18
相关论文
共 50 条
  • [1] Safety Barrier Certificates for Stochastic Hybrid Systems
    Lavaei, Abolfazl
    Soudjani, Sadegh
    Frazzoli, Emilio
    2022 AMERICAN CONTROL CONFERENCE, ACC, 2022, : 880 - 885
  • [2] Safety verification of hybrid systems using barrier certificates
    Prajna, S
    Jadbabaie, A
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2004, 2993 : 477 - 492
  • [3] A Simplex Architecture for Hybrid Systems Using Barrier Certificates
    Yang, Junxing
    Islam, Md. Ariful
    Murthy, Abhishek
    Smolka, Scott A.
    Stoller, Scott D.
    COMPUTER SAFETY, RELIABILITY, AND SECURITY, SAFECOMP 2017, 2017, 10488 : 117 - 131
  • [4] A logarithmic barrier approach for linear programming
    Menniche, Linda
    Benterki, Djamel
    JOURNAL OF COMPUTATIONAL AND APPLIED MATHEMATICS, 2017, 312 : 267 - 275
  • [5] Generating chaos for a class of linear switching control systems: A hybrid approach
    Zhang, Yuping
    Shi, Peng
    Zhu, Hong
    Hu, Jiangping
    Zeng, Yong
    JOURNAL OF THE FRANKLIN INSTITUTE-ENGINEERING AND APPLIED MATHEMATICS, 2015, 352 (12): : 5853 - 5865
  • [6] Safety Verification of Interconnected Hybrid Systems Using Barrier Certificates
    Wang, Guobin
    He, Jifeng
    Liu, Jing
    Sun, Haiying
    Ding, Zuohua
    Zhang, Miaomiao
    MATHEMATICAL PROBLEMS IN ENGINEERING, 2016, 2016
  • [7] Generating Invariant-Based Certificates for Embedded Systems
    Blech, Jan Olaf
    Perin, Michael
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2012, 11 (02)
  • [8] Hybrid Algorithm of Linear Programming Relaxation and Quantum Annealing
    Takabayashi, Taisei
    Ohzeki, Masayuki
    JOURNAL OF THE PHYSICAL SOCIETY OF JAPAN, 2024, 93 (03)
  • [9] Constructing Safety Barrier Certificates for Unknown Linear Optimal Control Systems
    Tooranjipour, Pouria
    Kiumarsi, Bahare
    2022 IEEE 17TH INTERNATIONAL CONFERENCE ON CONTROL & AUTOMATION, ICCA, 2022, : 213 - 219
  • [10] Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates
    Huang, Chao
    Chen, Xin
    Lin, Wang
    Yang, Zhengfeng
    Li, Xuandong
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2017, 16