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 条
  • [31] OBSERVATION WITH BOUNDS OF BIOLOGICAL SYSTEMS A Linear Programming Approach
    Tadeo, Fernando
    Rami, Mustapha Ait
    BIOSIGNALS 2010: PROCEEDINGS OF THE THIRD INTERNATIONAL CONFERENCE ON BIO-INSPIRED SYSTEMS AND SIGNAL PROCESSING, 2010, : 230 - 235
  • [32] A Linear Programming Approach for PAPR Reduction in OFDM Systems
    Tung, Yuan-Hao
    Lin, Kuhn-Chang
    Su, Yu T.
    2009 IEEE 20TH INTERNATIONAL SYMPOSIUM ON PERSONAL, INDOOR AND MOBILE RADIO COMMUNICATIONS, 2009, : 1667 - 1671
  • [33] A linear programming approach to the optimization of residential energy systems
    Lauinger, D.
    Caliandro, P.
    Van Herle, J.
    Kuhn, D.
    JOURNAL OF ENERGY STORAGE, 2016, 7 : 24 - 37
  • [34] An integer linear programming model for mapping applications on hybrid systems
    Theodoridis, G.
    Vassiliadis, N.
    Nikolaidis, S.
    IET COMPUTERS AND DIGITAL TECHNIQUES, 2009, 3 (01): : 33 - 42
  • [35] Actuator Scheduling for Linear Systems: A Convex Relaxation Approach
    Jiao, Junjie
    Maity, Dipankar
    Baras, John S.
    Hirche, Sandra
    IEEE CONTROL SYSTEMS LETTERS, 2022, 7 : 7 - 12
  • [36] An interactive hybrid programming approach to signals and systems laboratory
    Kehtarnavaz, N.
    Loizou, P.
    Rahman, M.
    2008 IEEE INTERNATIONAL CONFERENCE ON ACOUSTICS, SPEECH AND SIGNAL PROCESSING, VOLS 1-12, 2008, : 2633 - 2636
  • [37] Controller design approach based on linear programming
    Tanaka, Ryo
    Shibasaki, Hiroki
    Ogawa, Hiromitsu
    Murakami, Takahiro
    Ishida, Yoshihisa
    ISA TRANSACTIONS, 2013, 52 (06) : 744 - 751
  • [38] A hybrid approach of goal programming for weapon systems selection
    Lee, Jaewook
    Kang, Suk-Ho
    Rosenberger, Jay
    Kim, Seoung Bum
    COMPUTERS & INDUSTRIAL ENGINEERING, 2010, 58 (03) : 521 - 527
  • [39] A Hybrid approach for integer programming combining genetic algorithms, linear programming and ordinal optimization
    Yuh-Chyun Luo
    Monique Guignard
    Chun-Hung Chen
    Journal of Intelligent Manufacturing, 2001, 12 : 509 - 519
  • [40] A Hybrid approach for integer programming combining genetic algorithms, linear programming and ordinal optimization
    Luo, YC
    Guignard, M
    Chen, CH
    JOURNAL OF INTELLIGENT MANUFACTURING, 2001, 12 (5-6) : 509 - 519