Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
Publication:2331077
DOI10.1007/s10817-018-9497-xzbMath1468.68135OpenAlexW2891214311WikidataQ128901549 ScholiaQ128901549MaRDI QIDQ2331077
Andrew Sogokon, Taylor T. Johnson, Paul B. Jackson
Publication date: 25 October 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://eprints.soton.ac.uk/439288/1/Verifying_Safety_and_Persistence_in_Hybrid_Systems_Using_Flowpipes_and_Continuous_Invariants.pdf
hybrid systemsordinary differential equationsmetric temporal logicsafety verificationpositively invariant setsflowpipespersistence verification
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Attainable sets, reachability (93B03) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MetiTarski
- Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings
- Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11--18, 2015. Proceedings
- Cylindrical decomposition for systems transcendental in the first variable
- A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
- Computer aided verification. 20th international conference, CAV 2008, Princeton, NJ, USA, July 7--14, 2008. Proceedings
- MetiTarski: An automatic theorem prover for real-valued special functions
- Differential dynamic logic for hybrid systems
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
- Set invariance in control
- Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems
- Generating invariants for non-linear hybrid systems
- Hybrid systems: computation and control. 10th international conference, HSCC 2007, Pisa, Italy, April 3--5, 2007. Proceedings.
- Constructing invariants for hybrid systems
- A computational method for determining quadratic Lyapunov functions for non-linear systems
- Deadness and how to disprove liveness in hybrid dynamical systems
- Validated solutions of initial value problems for parametric ODEs
- A Method for Invariant Generation for Polynomial Continuous Systems
- Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- MetiTarski: Past and Future
- Deductive Verification of Continuous Dynamical Systems
- Hybrid Tools for Hybrid Systems – Proving Stability and Safety at Once
- Reachability Analysis of Nonlinear Systems Using Matrix Measures
- Automatic invariant generation for hybrid systems using ideal fixed points
- Lyapunov abstractions for inevitability of hybrid systems
- Stabhyli
- Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
- Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods
- Composing Stability Proofs for Hybrid Systems
- Recent Advances in Real Geometric Reasoning
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- Region Stability Proofs for Hybrid Systems
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Constraint-Based Approach for Analysis of Hybrid Systems
- Generating Box Invariants
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Systematic Simulation Using Sensitivity Analysis
- Hybrid automata: an insight into the discrete abstraction of discontinuous systems
- Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems
- Dynamical properties of hybrid automata
- Forward Inner-Approximated Reachability of Non-Linear Continuous Systems
- Hybrid Systems: Computation and Control
- Reach-Avoid Verification for Nonlinear Systems Based on Boundary Analysis
- On Taylor Model Based Integration of ODEs
- Some undecidable problems involving elementary functions of a real variable
- Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
- Hybrid Systems: Computation and Control
