Deductive stability proofs for ordinary differential equations
From MaRDI portal
Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by ordinary differential equations (93C15) Logic in computer science (03B70) Formalization of mathematics in connection with theorem provers (68V20) Stability theory for ordinary differential equations (34D99)
Abstract: Stability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of dL with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from dL's axioms with dL's ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on dL.
Recommendations
Cites work
- scientific article; zbMATH DE number 1201576 (Why is no real title available?)
- A complete uniform substitution calculus for differential dynamic logic
- A formal proof in Coq of Lasalle's invariance principle
- An axiomatic approach to existence and liveness for differential equations
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
- Bellerophon: tactical theorem proving for hybrid systems
- Differential equation invariance axiomatization
- Handbook of networked and embedded control systems.
- Hybrid Systems: Computation and Control
- Hybrid dynamical systems. Modeling, stability, and robustness
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- Local stability analysis using simulations and sum-of-squares programming
- Logical foundations of cyber-physical systems
- Nonlinear dynamical systems and control. A Lyapunov-based approach
- Nonlinear dynamics and chaos. With applications to physics, biology, chemistry, and engineering
- Nonlinear systems
- Ordinary differential equations with applications
- Simulation-guided Lyapunov analysis for hybrid dynamical systems
- Stability theory by Liapunov's direct method
- Switching in systems and control
- The Complete Proof Theory of Hybrid Systems
- The dynamical systems approach to differential equations
- The twisting tennis racket
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Verification of Hybrid Systems
Cited in
(5)- An axiomatic approach to existence and liveness for differential equations
- Notes on Recent Achievements in Proving Stability using KeYmaeraX
- A formal proof in Coq of Lasalle's invariance principle
- An axiomatic approach to liveness for differential equations
- Verifying Switched System Stability With Logic
This page was built for publication: Deductive stability proofs for ordinary differential equations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233505)
