An Axiomatic Approach to Liveness for Differential Equations

TL;DR

This paper introduces an axiomatic, deductive approach for verifying liveness properties of ordinary differential equations, addressing complexities like finite-time blow-up and convergence issues, and unifying various existing methods.

Contribution

It develops a general refinement framework for ODE liveness verification, corrects soundness errors in prior arguments, and facilitates the creation of new proof rules.

Findings

Unified framework for ODE liveness proofs

Corrected soundness errors in existing literature

Enabled development of new proof rules

Abstract

This paper presents an approach for deductive liveness verification for ordinary differential equations (ODEs) with differential dynamic logic. Numerous subtleties complicate the generalization of well-known 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. Our approach handles these subtleties by successively refining ODE liveness properties using ODE invariance properties which have a well-understood deductive proof theory. This approach is widely applicable: we survey several liveness arguments in the literature and derive them all as special instances of our axiomatic refinement approach. We also correct several soundness errors in the surveyed arguments, which further highlights the subtlety of ODE liveness reasoning and the utility of our deductive approach. The library of common refinement steps identified through our approach enables both the sound development and justification of new ODE liveness proof rules from our axioms.