TY - GEN
T1 - A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation
AU - Chen, Xin
AU - Peng, Chao
AU - Lin, Wang
AU - Yang, Zhengfeng
AU - Zhang, Yifang
AU - Li, Xuandong
N1 - Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
N2 - Barrier certificates generation is widely used in verifying safety properties of hybrid systems because of the relatively low computational complexity it costs. Under sum of squares (SOS) relaxation, the problem of barrier certificate generation is equivalent to that of solving a bilinear matrix inequality (BMI) with a particular type. The paper reveals the special feature of the problem, and adopts it to build a novel computational method. The proposed method introduces a sequential iterative scheme that is able to find analytical solutions, rather than the nonlinear solving procedure to produce numerical solutions used by general BMI solvers and thus is more efficient than them. In addition, different from popular LMI solving based methods, it does not make the verification conditions more conservative, and thus reduces the risk of missing feasible solutions. Benefitting from these two appealing features, it can produce barrier certificates not amenable to existing methods, which is supported by a complexity analysis as well as the experiment on some benchmarks.
AB - Barrier certificates generation is widely used in verifying safety properties of hybrid systems because of the relatively low computational complexity it costs. Under sum of squares (SOS) relaxation, the problem of barrier certificate generation is equivalent to that of solving a bilinear matrix inequality (BMI) with a particular type. The paper reveals the special feature of the problem, and adopts it to build a novel computational method. The proposed method introduces a sequential iterative scheme that is able to find analytical solutions, rather than the nonlinear solving procedure to produce numerical solutions used by general BMI solvers and thus is more efficient than them. In addition, different from popular LMI solving based methods, it does not make the verification conditions more conservative, and thus reduces the risk of missing feasible solutions. Benefitting from these two appealing features, it can produce barrier certificates not amenable to existing methods, which is supported by a complexity analysis as well as the experiment on some benchmarks.
KW - Barrier certificates
KW - Bilinear matrix inequalities
KW - Formal verification
KW - Hybrid systems
UR - https://www.scopus.com/pages/publications/85089210661
U2 - 10.1007/978-3-030-53288-8_29
DO - 10.1007/978-3-030-53288-8_29
M3 - 会议稿件
AN - SCOPUS:85089210661
SN - 9783030532871
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 582
EP - 603
BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
A2 - Lahiri, Shuvendu K.
A2 - Wang, Chao
PB - Springer
T2 - 32nd International Conference on Computer Aided Verification, CAV 2020
Y2 - 21 July 2020 through 24 July 2020
ER -