Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
This work addresses safety verification for semi-algebraic hybrid systems, offering a less conservative method that is still computationally tractable, though it appears incremental as it builds on existing barrier certificate approaches.
The authors tackled the problem of safety verification for hybrid systems by proposing a new Exponential Condition for barrier certificates, which reduces conservativeness while maintaining convexity, enabling verification of critical safety properties with examples demonstrating effectiveness.
A barrier certificate is an inductive invariant function which can be used for the safety verification of a hybrid system. Safety verification 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 certificate condition, called Exponential Condition, for the safety verification 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 convexity guarantees its solvability by semidefinite programming method. Some examples are presented to illustrate the effectiveness and practicality of our method.