An axiomatic approach to existence and liveness for differential equations

DOI10.1007/s00165-020-00525-0OpenAlexW3153326561WikidataQ115389095 ScholiaQ115389095MaRDI QIDQ1982634

Yong Kiam Tan, André Platzer

Publication date: 14 September 2021

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2004.14561

zbMATH Keywords

livenessdifferential equationsglobal existencedifferential dynamic logic

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (3)

A program logic to verify signal temporal logic specifications of hybrid systems ⋮ Deductive stability proofs for ordinary differential equations ⋮ Implicit definitions with differential equations for KeYmaera X (system description)

Uses Software

• KeYmaera
• SpaceEx
• LySHA
• Flow*
• Bellerophon
• KeYmaera X

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Understanding deadlock and livelock behaviors in hybrid control systems
• First-order dynamic logic
• Bellerophon: tactical theorem proving for hybrid systems
• A complete uniform substitution calculus for differential dynamic logic
• Hybrid action systems
• \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
• Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
• Computability with polynomial differential equations
• Zeno hybrid systems
• Lyapunov abstractions for inevitability of hybrid systems
• Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
• Verification of Hybrid Systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Convex Programs for Temporal Verification of Nonlinear Dynamical Systems
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Proving Liveness Properties of Concurrent Programs
• Refinement Calculus
• Differential Refinement Logic
• Logical Foundations of Cyber-Physical Systems
• Boundedness of the Domain of Definition is Undecidable for Polynomial ODEs
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Differential Equation Invariance Axiomatization
• Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems
• Forward Inner-Approximated Reachability of Non-Linear Continuous Systems
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• Differential Hybrid Games
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control

This page was built for publication: An axiomatic approach to existence and liveness for differential equations