Barrier certificates revisited

DOI10.1016/j.jsc.2016.07.010zbMath1357.68110arXiv1310.6481OpenAlexW1627251346MaRDI QIDQ507352

Ting Gan, Bican Xia, Liyun Dai, Naijun Zhan

Publication date: 6 February 2017

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

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

zbMATH Keywords

nonlinear systemformal verificationinvariantsemi-definite programminghybrid systemsum of squaresbarrier certificate

Mathematics Subject Classification ID

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

Related Items (15)

Synthesizing invariant barrier certificates via difference-of-convex programming ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Pegasus: sound continuous invariant generation ⋮ Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems ⋮ Sufficient conditions for forward invariance and contractivity in hybrid inclusions using barrier functions ⋮ 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 ⋮ Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems ⋮ FOSSIL ⋮ Vector barrier certificates and comparison systems ⋮ Learning safe neural network controllers with barrier certificates ⋮ Automated and formal synthesis of neural barrier certificates for dynamical models ⋮ Smaller SDP for SOS decomposition ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming

Uses Software

• Sostools
• RSOLVER
• Benchmarks
• dReal
• HSolver
• Flow*

Cites Work

• The algorithmic analysis of hybrid systems
• Exact safety verification of hybrid systems using sums-of-squares representation
• Computing differential invariants of hybrid systems as fixed points
• Semidefinite programming relaxations for semialgebraic problems
• Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients
• Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
• Generating Non-linear Interpolants by Semidefinite Programming
• Solving Non-linear Arithmetic
• 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
• Constraint-Based Approach for Analysis of Hybrid Systems
• SOSTOOLS and Its Control Applications
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Symbolic reachability computation for families of linear vector fields

This page was built for publication: Barrier certificates revisited