Exact safety verification of hybrid systems using sums-of-squares representation  

作　　者：LIN Wang WU Min YANG ZhengFeng ZENG ZhenBing 

机构地区：[1]Shanghai Key Laboratory of Trustworthy Computing, East China Normal University [2]College of Mathematics and Information Science, Wenzhou University

出　　处：《Science China(Information Sciences)》2014年第5期16-28,共13页中国科学（信息科学）（英文版）

基　　金：supported in part by National Natural Science Foundation of China(Grant Nos.61021004,91118007,10801052,10901055);Fundamental Research Funds for the Central Universities(Grant No.78210043);NKBRPC(Grant No.2011CB302802);Scientific Research Project of The Graduate School of East China Normal University(Grant No.CX2011009)

摘　　要：In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares （SOS） relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares （SOS） relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.

关 键 词：Symbolic computation semidefinite programming safety verification invariant generation 

分 类 号：O19[理学—数学]