Verification of continuous dynamical systems by timed automata

DOI10.1007/S10703-011-0118-0MaRDI QIDQ763240zbMATH OpenOpenAlexFDO

Authors Christoffer Sloth, Rafał Wisniewski

Publication date 9 March 2012

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://vbn.aau.dk/ws/files/56661348/Verification_of_continuous_dynamical_systems_by_timed_automata.pdf

zbMATH Keywords

verificationLyapunov functionsreachabilitytimed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Stability of topological dynamical systems (37B25) Dynamics induced by flows and semiflows (37C10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verified model checking of timed automata
• Approximating Continuous Systems by Timed Automata
• Verification of timed automata via satisfiability checking
• Verifying continuous-time duration calculus against real-time automaton
• Verified certification of reachability checking for timed automata
• Formal Modeling and Analysis of Timed Systems
• Publication:4508304
• Dynamical Properties of Timed Automata Revisited
• Dynamically-driven timed automaton abstractions for proving liveness of continuous systems

Cites work

• scientific article; zbMATH DE number 425858 (Why is no real title available?)
• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 1113627 (Why is no real title available?)
• scientific article; zbMATH DE number 1956618 (Why is no real title available?)
• scientific article; zbMATH DE number 1863183 (Why is no real title available?)
• scientific article; zbMATH DE number 2229941 (Why is no real title available?)
• A theory of timed automata
• Abstractions for hybrid systems
• An introduction to Morse theory. Transl. from the Japanese by Kiki Hudson and Masahico Saito
• Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems
• Approximating Continuous Systems by Timed Automata
• Energy Functions for Morse Smale Systems
• Geometric analysis of nondeterminacy in dynamical systems
• Hybrid Systems: Computation and Control
• Linear Matrix Inequalities in System and Control Theory
• Structural stability on two-dimensional manifolds
• Verification, performance analysis and controller synthesis for real-time systems

Cited in

(12)

• Proving properties of continuous systems: Qualitative simulation and temporal logic
• Convex Programs for Temporal Verification of Nonlinear Dynamical Systems
• Complete abstractions of dynamical systems by timed automata
• On the determinization of timed systems
• Timed-automata abstraction of switched dynamical systems using control invariants
• Dynamical properties of timed automata
• Timed-automata abstraction of switched dynamical systems using control funnels
• Verification of \(N\)-\(M\) switching control system: a case study in temporal logic model checking
• Deadness and how to disprove liveness in hybrid dynamical systems
• Dynamically-driven timed automaton abstractions for proving liveness of continuous systems
• A menagerie of timed automata
• Using symmetry transformations in equivariant dynamical systems for their safety verification

Describes a project that uses

Uses Software

• Uppaal

This page was built for publication: Verification of continuous dynamical systems by timed automata

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