Barrier certificates revisited
From MaRDI portal
Publication:507352
DOI10.1016/J.JSC.2016.07.010zbMATH Open1357.68110arXiv1310.6481OpenAlexW1627251346MaRDI QIDQ507352FDOQ507352
Ting Gan, Bican Xia, Liyun Dai, Naijun Zhan
Publication date: 6 February 2017
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
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
Full work available at URL: https://arxiv.org/abs/1310.6481
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
hybrid systemnonlinear systeminvariantsum of squaresformal verificationsemi-definite programmingbarrier certificate
Symbolic computation and algebraic computation (68W30) Semidefinite programming (90C22) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Hybrid Systems: Computation and Control
- Semidefinite programming relaxations for semialgebraic problems
- SOSTOOLS and Its Control Applications
- A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
- Hybrid Systems: Computation and Control
- The algorithmic analysis of hybrid systems
- Solving Non-linear Arithmetic
- Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients
- Computing differential invariants of hybrid systems as fixed points
- Constraint-Based Approach for Analysis of Hybrid Systems
- Symbolic reachability computation for families of linear vector fields
- Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
- Generating Non-linear Interpolants by Semidefinite Programming
- Deductive verification of continuous dynamical systems
- Formal Modelling, Analysis and Verification of Hybrid Systems
- Automatic invariant generation for hybrid systems using ideal fixed points
- Compositional safety analysis using barrier certificates
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Hybrid Systems: Computation and Control
- Exact safety verification of hybrid systems using sums-of-squares representation
Cited In (17)
- Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
- Vector barrier certificates and comparison systems
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Pegasus: sound continuous invariant generation
- 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
- Smaller SDP for SOS decomposition
- Automated and formal synthesis of neural barrier certificates for dynamical models
- Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
- Sufficient conditions for forward invariance and contractivity in hybrid inclusions using barrier functions
- Hybrid Systems: Computation and Control
- Learning safe neural network controllers with barrier certificates
- Pegasus: a framework for sound continuous invariant generation
- FOSSIL
- Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems
- Synthesizing invariant barrier certificates via difference-of-convex programming
Uses Software
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)
