Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems

DOI10.1007/978-3-319-19249-9_32zbMath1427.68174OpenAlexW2168048876MaRDI QIDQ5206959

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

Mathematics Subject Classification ID

Nonlinear ordinary differential equations and systems (34A34) Specification and verification (program logics, model checking, etc.) (68Q60) Hybrid systems of ordinary differential equations (34A38)

Related Items (4)

A program logic to verify signal temporal logic specifications of hybrid systems ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Differential dynamic logic for hybrid systems
• Defining liveness
• Real quantifier elimination is doubly exponential
• Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
• Set invariance in control
• An invariant-based approach to the design of hybrid control systems
• Deductive Verification of Continuous Dynamical Systems
• Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Proving Liveness Properties of Concurrent Programs
• Proving the Correctness of Multiprocess Programs
• Hybrid automata: an insight into the discrete abstraction of discontinuous systems
• Hybrid Systems: Computation and Control
• Polynomial Level-Set Method for Polynomial System Reachable Set Estimation
• Automated Technology for Verification and Analysis
• On Taylor Model Based Integration of ODEs
• Some undecidable problems involving elementary functions of a real variable
• The solution of minimaximin problems
• Hybrid Systems: Computation and Control
• Set-theoretic methods in control

This page was built for publication: Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems