Deductive Stability Proofs for Ordinary Differential Equations

TL;DR

This paper introduces a formal method using differential dynamic logic to verify the stability of systems modeled by ordinary differential equations, enabling rigorous proofs and analysis of stability properties.

Contribution

It presents a novel approach to specify and verify ODE stability within differential dynamic logic, enhancing formal analysis capabilities.

Findings

Formal specification of ODE stability using nested modalities and quantifiers

Rigorous proofs of stability properties derived from dL axioms

Implementation of stability proofs in the KeYmaera X theorem prover

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.