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

DOI10.1007/978-3-642-39799-8_17zbMATH Open1357.68113arXiv1303.6885OpenAlexW2129729773MaRDI QIDQ2864837FDOQ2864837

Authors: Hui Kong, Fei He, Xiaoyu Song, William N. N. Hung, Ming Gu 

Publication date: 26 November 2013

Published in: Computer Aided Verification (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1303.6885

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

zbMATH Keywords

hybrid systemnonlinear systemsafety verificationsum of squaresbarrier certificateinductive invariant

Mathematics Subject Classification ID

Semidefinite programming (90C22) Specification and verification (program logics, model checking, etc.) (68Q60)

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
• Hybrid Systems: Computation and Control
• Safety verification of interconnected hybrid systems using barrier certificates
• 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
• On converse zeroing barrier functions
• Barrier certificates revisited
• Pegasus: a framework for sound continuous invariant generation
• FOSSIL
• Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems
• Verifying Neural Network Controlled Systems Using Neural Networks
• Synthesizing invariant barrier certificates via difference-of-convex programming

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)