Dynamically-driven timed automaton abstractions for proving liveness of continuous systems

DOI10.1007/978-3-642-33365-1_6MaRDI QIDQ4649386zbMATH OpenOpenAlexFDO

Authors Rebekah Carter, Eva María Navarro-López

Publication date 21 November 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-33365-1_6

zbMATH Keywords

abstractionautomated verificationcontinuous-time systemsliveness propertiestimed automata

Mathematics Subject Classification ID

Symbolic dynamics (37B10) Formal languages and automata (68Q45)

Recommendations

• Lyapunov abstractions for inevitability of hybrid systems
• Direct formal verification of liveness properties in continuous and hybrid dynamical systems
• Approximating Continuous Systems by Timed Automata
• Complete abstractions of dynamical systems by timed automata
• Verification of continuous dynamical systems by timed automata

Cited in

(8)

• Presburger liveness verification of discrete timed automata.
• Deadness and how to disprove liveness in hybrid dynamical systems
• Lyapunov abstractions for inevitability of hybrid systems
• scientific article; zbMATH DE number 1538037 (Why is no real title available?)
• Direct formal verification of liveness properties in continuous and hybrid dynamical systems
• An axiomatic approach to liveness for differential equations
• Reachability in dynamical systems with rounding
• Verification of continuous dynamical systems by timed automata

This page was built for publication: Dynamically-driven timed automaton abstractions for proving liveness of continuous systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649386)