Deductive stability proofs for ordinary differential equations
From MaRDI portal
Logic in computer science (03B70) Stability theory for ordinary differential equations (34D99) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20) Control/observation systems governed by ordinary differential equations (93C15)
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
- 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.
- scientific article; zbMATH DE number 1201576 (Why is no real title available?)
- Hybrid dynamical systems. Modeling, stability, and robustness
- Hybrid Systems: Computation and Control
- 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
(6)- A formal proof in Coq of Lasalle's invariance principle
- An axiomatic approach to existence and liveness for differential equations
- Notes on Recent Achievements in Proving Stability using KeYmaeraX
- Verifying Switched System Stability With Logic
- An axiomatic approach to liveness for differential equations
- Differential elimination and algebraic invariants of polynomial dynamical systems
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)
