A New Barrier Certificate for Safety Verification of Hybrid Systems

作者：Kong Hui^*; Song Xiaoyu; Han Dong; Gu Ming; Sun Jiaguang

来源：Computer Journal, 2014, 57(7): 1033-1045.

DOI：10.1093/comjnl/bxt059

• inductive invariant
• barrier certificate
• safety verification
• hybrid system
• non-linear system
• sum of squares

A barrier certificate is an inductive invariant of functions which can be used to prove the safety property of a hybrid system. Utilizing a barrier certificate has the benefit of avoiding explicit computation of the exact reachable set which is usually not tractable for non-linear hybrid systems. In this paper, we propose a new barrier certificate condition, called Exponential Condition, for the safety verification of semialgebraic hybrid systems. The main important benefit of Exponential Condition is that it has a lower conservativeness than the existing convex conditions and meanwhile it possesses the convexity. On the one hand, a less conservative barrier certificate forms a tighter over-approximation for the reachable set and hence is able to verify critical safety properties. On the other hand, the convexity guarantees its solvability by a semidefinite programming method. Some examples are presented to illustrate the effectiveness and practicality of our method.

• 出版日期2014-7
• 单位中国科学院声学研究所; 清华大学