M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems

Abstract. A barrier certificate is an inductive invariant function which can be used for the safety verification of a hybrid system. Safety veri-fication based on barrier certificate has the benefit of avoiding explicit computation of the exact reachable set which is usually intractable for nonlinear hybrid systems. In this paper, we propose a new barrier cer-tificate condition, called Exponential Condition, for the safety verifica-tion of semi-algebraic hybrid systems. The most important benefit of Exponential Condition is that it has a lower conservativeness than the existing convex condition and meanwhile it possesses the property of 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 property of con-vexity guarantees its solvability by semidefinite programming method. Some examples are presented to illustrate the effectiveness and practi-cality of our method