Exact safety verification of hybrid systems using sums-of-squares representation
From MaRDI portal
Publication:893625
DOI10.1007/S11432-013-4961-ZzbMATH Open1343.93051arXiv1112.2328OpenAlexW2066257627MaRDI QIDQ893625FDOQ893625
Authors: N. E. Zubov 
Publication date: 20 November 2015
Published in: Science China Information Sciences (Search for Journal in Brave)
Abstract: In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is deployed to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.
Full work available at URL: https://arxiv.org/abs/1112.2328
Recommendations
- Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients
- Safety verification of nonlinear hybrid systems based on invariant clusters
- Constructing invariants for hybrid systems
- Safety verification of hybrid systems using certified multiple Lyapunov-like functions
- Transcendental inductive invariants generation for non-linear differential and hybrid systems
Semidefinite programming (90C22) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)
Cites Work
- Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
- QEPCAD B
- Hybrid Systems: Computation and Control
- Differential dynamic logic for hybrid systems
- Hybrid Systems: Computation and Control
- Moments, positive polynomials and their applications
- Hybrid Systems: Computation and Control
- Computational techniques for hybrid system verification
- Constructing invariants for hybrid systems
- The algorithmic analysis of hybrid systems
- Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients
- Input-to-state stability of switched nonlinear systems
- Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients
- The Image Computation Problem in Hybrid Systems Model Checking
- The Computational Complexity of Simultaneous Diophantine Approximation Problems
- 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
- Verification and synthesis using real quantifier elimination
- Deductive verification of continuous dynamical systems
- Automatic invariant generation for hybrid systems using ideal fixed points
- Hybrid Systems: Computation and Control
- Title not available (Why is that?)
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Morphisms for Non-trivial Non-linear Invariant Generation for Algebraic Hybrid Systems
- Stability of linear discrete switched systems with delays based on average dwell time method
Cited In (6)
- Computation of verified Lyapunov functions of hybrid systems by a symbolic-numeric method
- Safety verification of nonlinear hybrid systems based on invariant clusters
- Safety verification of hybrid systems using certified multiple Lyapunov-like functions
- Automated Machine-Checked Hybrid System Safety Proofs
- Barrier certificates revisited
- Synthesizing switching controllers for hybrid systems by generating invariants
Uses Software
This page was built for publication: Exact safety verification of hybrid systems using sums-of-squares representation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q893625)
