Direct formal verification of liveness properties in continuous and hybrid dynamical systems
From MaRDI portal
Publication:5206959
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
Cites work
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 1302474 (Why is no real title available?)
- scientific article; zbMATH DE number 1507210 (Why is no real title available?)
- scientific article; zbMATH DE number 3337915 (Why is no real title available?)
- scientific article; zbMATH DE number 2226273 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- scientific article; zbMATH DE number 3100403 (Why is no real title available?)
- An invariant-based approach to the design of hybrid control systems
- Automated Technology for Verification and Analysis
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Deductive verification of continuous dynamical systems
- Defining liveness
- Differential dynamic logic for hybrid systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid automata: an insight into the discrete abstraction of discontinuous systems
- On Taylor Model Based Integration of ODEs
- Polynomial Level-Set Method for Polynomial System Reachable Set Estimation
- Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
- Proving Liveness Properties of Concurrent Programs
- Proving the Correctness of Multiprocess Programs
- Real quantifier elimination is doubly exponential
- Set invariance in control
- Set-theoretic methods in control
- Some undecidable problems involving elementary functions of a real variable
- The solution of minimaximin problems
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
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
- scientific article; zbMATH DE number 177518 (Why is no real title available?)
- Proving Liveness and Termination of Systolic Arrays Using Communicating Finite State Machines
- A program logic to verify signal temporal logic specifications of hybrid systems
- scientific article; zbMATH DE number 177525 (Why is no real title available?)
- 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)
