An Axiomatic Approach to Existence and Liveness for Differential Equations
share
This article presents an axiomatic approach for deductive verification of existence and liveness for ordinary differential equations (ODEs) with differential dynamic logic (dL). The approach yields proofs that the solution of a given ODE exists long enough to reach a given target region without leaving a given evolution domain. Numerous subtleties complicate the generalization of discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions may blow up in finite time or their progress towards the goal may converge to zero. These subtleties are handled in dL by successively refining ODE liveness properties using ODE invariance properties which have a well-understood deductive proof theory. This approach is widely applicable: several liveness arguments from the literature are surveyed and derived as special instances of axiomatic refinement in dL. These derivations also identify and correct several soundness errors in the surveyed literature, which further highlights the subtlety of ODE liveness reasoning and the utility of an axiomatic deductive approach. An important special case of the approach yields formal deduction of (global) existence properties of ODEs, which are a fundamental part of every ODE liveness argument. Thus, all generalizations of existence properties and their proofs immediately lead to corresponding generalizations of ODE liveness arguments. Overall, the resulting library of common refinement steps enables both the sound development and justification of new ODE existence and liveness proof rules from dL axioms. These insights also enable and inform an implementation of those proof rules in the KeYmaera X theorem prover for hybrid systems.
READ FULL TEXT