Direct formal verification of liveness properties in continuous and hybrid dynamical systems
DOI10.1007/978-3-319-19249-9_32zbMATH Open1427.68174OpenAlexW2168048876MaRDI QIDQ5206959FDOQ5206959
Authors: Andrew Sogokon, Paul B. Jackson 
Publication date: 19 December 2019
Published in: FM 2015: Formal Methods (Search for Journal in Brave)
Full work available at URL: https://www.pure.ed.ac.uk/ws/files/19596664/Sogokon_Jackson_2015_Direct_formal_verification_of_liveness_properties_in_continuous_and_hybrid_dynamical_systems.pdf
Recommendations
- Dynamically-driven timed automaton abstractions for proving liveness of continuous systems
- Monitoring bounded LTL properties using interval analysis
- Hybrid diagrams: a deductive-algorithmic approach to hybrid system verification
- Proving properties of continuous systems: Qualitative simulation and temporal logic
- An axiomatic approach to existence and liveness for differential equations
Nonlinear ordinary differential equations and systems (34A34) Specification and verification (program logics, model checking, etc.) (68Q60) Hybrid systems of ordinary differential equations (34A38)
Cites Work
- Differential dynamic logic for hybrid systems
- Set invariance in control
- Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
- Hybrid Systems: Computation and Control
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Set-theoretic methods in control
- Some undecidable problems involving elementary functions of a real variable
- Title not available (Why is that?)
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
- Title not available (Why is that?)
- Real quantifier elimination is doubly exponential
- On Taylor Model Based Integration of ODEs
- Title not available (Why is that?)
- Defining liveness
- Proving the Correctness of Multiprocess Programs
- Proving Liveness Properties of Concurrent Programs
- An invariant-based approach to the design of hybrid control systems
- Deductive verification of continuous dynamical systems
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Hybrid Systems: Computation and Control
- Automated Technology for Verification and Analysis
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Title not available (Why is that?)
- Hybrid automata: an insight into the discrete abstraction of discontinuous systems
- Polynomial Level-Set Method for Polynomial System Reachable Set Estimation
- The solution of minimaximin problems
Cited In (14)
- An axiomatic approach to existence and liveness for differential equations
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Deadness and how to disprove liveness in hybrid dynamical systems
- Monitoring bounded LTL properties using interval analysis
- Lyapunov abstractions for inevitability of hybrid systems
- Title not available (Why is that?)
- Proving Liveness and Termination of Systolic Arrays Using Communicating Finite State Machines
- A program logic to verify signal temporal logic specifications of hybrid systems
- Title not available (Why is that?)
- A Fast Verified Liveness Analysis in SSA Form
- Liveness characterization for GFC systems. II
- Dynamically-driven timed automaton abstractions for proving liveness of continuous systems
- An axiomatic approach to liveness for differential equations
- ModelPlex: verified runtime validation of verified cyber-physical system models
This page was built for publication: Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5206959)
