An Axiomatic Approach to Liveness for Differential Equations
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.
KeywordsDifferential equations Liveness Differential dynamic logic
We thank Katherine Cordwell, Frank Pfenning, Andrew Sogokon, and the anonymous reviewers for their feedback on this paper. This material is based upon work supported by the Alexander von Humboldt Foundation and the AFOSR under grant number FA9550-16-1-0288. The first author was also supported by A*STAR, Singapore.
- 2.Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)Google Scholar
- 7.Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: Dang, T., Mitchell, I.M. (eds.) HSCC, pp. 115–124. ACM, New York (2012). https://doi.org/10.1145/2185632.2185652
- 14.Papachristodoulou, A., Prajna, S.: On the construction of Lyapunov functions using the sum of squares decomposition. In: CDC, vol. 3, pp. 3482–3487. IEEE (2002). https://doi.org/10.1109/CDC.2002.1184414
- 16.Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13–24. IEEE (2012). https://doi.org/10.1109/LICS.2012.13
- 26.Sogokon, A., Jackson, P.B., Johnson, T.T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants. J. Autom. Reas. (2018, to appear). https://doi.org/10.1007/s10817-018-9497-x
- 28.Tan, Y.K., Platzer, A.: An axiomatic approach to liveness for differential equations. CoRR abs/1904.07984 (2019)Google Scholar