Abstract: A barrier certificate can separate the state space of a con- sidered hybrid system (HS) into safe and unsafe parts ac- cording to the safety property to be verified. Therefore this notion has been widely used in the verification of HSs. A stronger condition on barrier certificates means that less expressive barrier certificates can be synthesized. On the other hand, synthesizing more expressive barrier certificates often means high complexity. In [9], Kong et al consid- ered how to relax the condition of barrier certificates while still keeping their convexity so that one can synthesize more expressive barrier certificates efficiently using semi-definite programming (SDP). In this paper, we first discuss how to relax the condition of barrier certificates in a general way, while still keeping their convexity. Particularly, one can then utilize different weaker conditions flexibly to synthesize dif- ferent kinds of barrier certificates with more expressiveness efficiently using SDP. These barriers give more opportuni- ties to verify the considered system. We also show how to combine two functions together to form a combined barrier certificate in order to prove a safety property under consid- eration, whereas neither of them can be used as a barrier certificate separately, even according to any relaxed condi- tion. Another contribution of this paper is that we discuss how to discover certificates from the general relaxed condi- tion by SDP. In particular, we focus on how to avoid the unsoundness because of numeric error caused by SDP with symbolic checking
Recommendations
- Converse Barrier Certificate Theorems
- Vector barrier certificates and comparison systems
- A novel approach for solving the BMI problem in barrier certificates generation
- Barrier certificates for nonlinear model validation
- Converse Theorems for Safety and Barrier Certificates
- Synthesizing barrier certificates using neural networks
- Barrier solutions
- Compositional safety analysis using barrier certificates
- Barrier coverage
- Synthesizing invariant barrier certificates via difference-of-convex programming
Cites work
- A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
- Automatic invariant generation for hybrid systems using ideal fixed points
- Compositional safety analysis using barrier certificates
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Computing differential invariants of hybrid systems as fixed points
- Constraint-Based Approach for Analysis of Hybrid Systems
- Deductive verification of continuous dynamical systems
- Exact safety verification of hybrid systems using sums-of-squares representation
- Exponential-condition-based barrier certificate generation for safety verification of hybrid systems
- Formal modelling, analysis and verification of hybrid systems
- Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients
- Generating non-linear interpolants by semidefinite programming
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- SOSTOOLS and Its Control Applications
- Semidefinite programming relaxations for semialgebraic problems
- Solving non-linear arithmetic
- Symbolic reachability computation for families of linear vector fields
- The algorithmic analysis of hybrid systems
- dReal: an SMT solver for nonlinear theories over the reals
Cited in
(20)- Synthesizing invariant barrier certificates via difference-of-convex programming
- Automated and formal synthesis of neural barrier certificates for dynamical models
- Safe reward‐based deep reinforcement learning control for an electro‐hydraulic servo system
- Vector Control Lyapunov and Barrier Functions for Safe Stabilization of Interconnected Systems
- Sufficient conditions for forward invariance and contractivity in hybrid inclusions using barrier functions
- A linear programming relaxation based approach for generating barrier certificates of hybrid systems
- Exponential-condition-based barrier certificate generation for safety verification of hybrid systems
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
- Smaller SDP for SOS decomposition
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Pegasus: a framework for sound continuous invariant generation
- A novel approach for solving the BMI problem in barrier certificates generation
- Hybrid Systems: Computation and Control
- Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- Pegasus: sound continuous invariant generation
- Vector barrier certificates and comparison systems
- Learning safe neural network controllers with barrier certificates
- FOSSIL
- Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems
This page was built for publication: Barrier certificates revisited
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q507352)
