Exponential-condition-based barrier certificate generation for safety verification of hybrid systems
From MaRDI portal
Publication:2864837
Abstract: 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.
Recommendations
- Barrier certificates revisited
- Hybrid Systems: Computation and Control
- Synthesizing invariant barrier certificates via difference-of-convex programming
- Safety verification of interconnected hybrid systems using barrier certificates
- A linear programming relaxation based approach for generating barrier certificates of hybrid systems
Cited in
(26)- Linearization, model reduction and reachability in nonlinear ODEs
- Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
- Implicit semi-algebraic abstraction for polynomial dynamical systems
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
- Vector barrier certificates and comparison systems
- A novel approach for solving the BMI problem in barrier certificates generation
- A linear programming relaxation based approach for generating barrier certificates of hybrid systems
- Pegasus: sound continuous invariant generation
- Automated and formal synthesis of neural barrier certificates for dynamical models
- Sufficient conditions for forward invariance and contractivity in hybrid inclusions using barrier functions
- Hybrid Systems: Computation and Control
- Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares programming
- Safety verification for distributed parameter systems using barrier functionals
- Safety verification of interconnected hybrid systems using barrier certificates
- Hybrid Systems: Computation and Control
- An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems
- Hybrid Systems: Computation and Control
- Sufficient conditions for robust safety in differential inclusions using barrier functions
- Learning safe neural network controllers with barrier certificates
- Barrier certificates revisited
- On converse zeroing barrier functions
- Pegasus: a framework for sound continuous invariant generation
- Synthesizing invariant barrier certificates via difference-of-convex programming
- FOSSIL
- Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems
- Verifying Neural Network Controlled Systems Using Neural Networks
This page was built for publication: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864837)
