Abstract
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 complete axiomatization. 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 correct several soundness errors in the surveyed literature, which further highlights the subtlety of ODE liveness reasoning and the utility of an axiomatic approach. An important special case of this approach deduces (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 of liveness proof rules from dL axioms. These insights are put into practice through an implementation of ODE liveness proofs in the KeYmaera X theorem prover for hybrid systems.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abate A, D'Innocenzo A, Di Benedetto MD, Sastry S(2009) Understanding deadlock and livelock behaviors in hybrid control systems. Nonlinear Anal Hybrid Syst 3(2):150–162. https://doi.org/10.1016/j.nahs.2008.12.005
Alur, R.: Principles of cyber-physical systems. MIT Press, Cambridge (2015)
Butler MJ, Abrial J-R, Banach R (2016) Modelling and refining hybrid systems in Event-B and Rodin. In: Petre L, Sekerinski E (eds) From action systems to distributed systems—the refinement approach. Chapman and Hall/CRC, Boca Raton, pp 29–42. https://doi.org/10.1201/b20053
Bochnak J, Coste M, Roy M-F (1998) Real algebraic geometry. Springer, Heidelberg. https://doi.org/10.1007/978-3-662-03718-8
Bohrer B, Fernández M, Platzer A (2019) dL\(_\iota \): Definite descriptions in differential dynamic logic. In: Fontaine P (ed) CADE, volume 11716 of LNCS. Springer, Cham, pp 94–110. https://doi.org/10.1007/978-3-030-29436-6_6
Bohrer B, Tan YK, Mitsch S, Sogokon A, Platzer A (2019) A formal safety net for waypoint-following in ground robots. IEEE Robot Autom Lett 4(3):2910–2917. https://doi.org/10.1109/LRA.2019.2923099
Back R-J, von Wright J (1998) Refinement calculus—a systematic introduction. Springer, Berlin. https://doi.org/10.1007/978-1-4612-1674-2
Chen X, Ábrahám E, Sankaranarayanan S (2013) Flow*: an analyzer for non-linear hybrid systems. In: Sharygina N, Veith H (eds) CAV, volume 8044 of LNCS. Springer, Heidelberg, pp 258–263. https://doi.org/10.1007/978-3-642-39799-8_18
Chicone C (2006) Ordinary differential equations with applications, 2nd ed. Springer, New York. https://doi.org/10.1007/0-387-35794-7
Dupont G, Ameur Y, Pantel M, Singh NK (2019) Handling refinement of continuous behaviors: a proof based approach with Event-B. In: Méry D, Qin S (eds) TASE. IEEE, pp 9–16. https://doi.org/10.1109/TASE.2019.00-25
Doyen L, Frehse G, Pappas GJ, Platzer A (2018) Verification of hybrid systems. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of model checking. Springer, Cham, pp 1047–1110. https://doi.org/10.1007/978-3-319-10575-8_30
Duggirala PS, Mitra S (2012) Lyapunov abstractions for inevitability of hybrid systems. In: Dang T, Mitchell IM (eds) HSCC. ACM, New York, pp 115–124. https://doi.org/10.1145/2185632.2185652
Frehse G, Guernic CL, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan G, Qadeer S (eds) CAV, volume 6806 of LNCS. Springer, Heidelberg, pp 379–395. https://doi.org/10.1007/978-3-642-22110-1_30
Fulton N, Mitsch S, Bohrer B, Platzer A (2017) Bellerophon: tactical theorem proving for hybrid systems. In: Ayala-Rincón M, Muñoz CA (eds) ITP, volume 10499 of LNCS. Springer, Cham, pp 207–224. https://doi.org/10.1007/978-3-319-66107-0_14
Fulton N, Mitsch S, Quesel J-D, Völp M, Platzer A (2015) KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty AP, Middeldorp A (eds) CADE, volume 9195 of LNCS. Springer, Cham, pp 527–538. https://doi.org/10.1007/978-3-319-21401-6_36
Foster S, y Munive JJH, Struth G(2020) Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. In: Fahrenberg U, Jipsen P, Winter M (eds) RAMiCS, volume 12062 of LNCS. Springer, pp 169–186. https://doi.org/10.1007/978-3-030-43520-2_11
Graça DS, Buescu J, Campagnolo ML (2008) Boundedness of the domain of definition is undecidable for polynomial ODEs. Electron Notes Theor Comput Sci 202:49–57. https://doi.org/10.1016/j.entcs.2008.03.007
Graça DS, Campagnolo ML, Buescu J (2008) Computability with polynomial differential equations. Adv Appl Math 40(3):330–349. https://doi.org/10.1016/j.aam.2007.02.003
Ghorbal K, Platzer A (2014) Characterizing algebraic invariants by differential radical invariants. In: Ábrahám E, Havelund K (eds) TACAS, volume 8413 of LNCS. Springer, Heidelberg, pp 279–294. https://doi.org/10.1007/978-3-642-54862-8_19
Goubault E, Putot S (2017) Forward inner-approximated reachability of non-linear continuous systems. In: Frehse G, Mitra S (eds) HSCC. ACM, New York, pp 1–10. https://doi.org/10.1145/3049797.3049811
Harel D (1979) First-order dynamic logic, volume 68 of LNCS. Springer. https://doi.org/10.1007/3-540-09237-4
Haddad, W.M., Chellaboina, V.: Nonlinear dynamical systems and control: a Lyapunov-based approach. Princeton University Press, Princeton (2008)
Henzinger TA (1996) The theory of hybrid automata. In: LICS. IEEE Computer Society, pp 278–292. https://doi.org/10.1109/LICS.1996.561342
Khalil, H.K.: Nonlinear systems. Macmillan Publishing Company, New York (1992)
Kozen D (1997) Kleene algebra with tests. ACM Trans Program Lang Syst 19(3):427–443. https://doi.org/10.1145/256167.256195
Logic in Computer Science (LICS): 27th Annual IEEE symposium on. Los Alamitos, IEEE (2012)
Loos SM, Platzer A (2016) Differential refinement logic. In: Grohe M, Koskinen E, Shankar N (eds) LICS. ACM, pp 505–514. https://doi.org/10.1145/2933575.2934555
Liu J, Zhan N, Zhao H (2011) Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty S, Jerraya A, Baruah SK, Fischmeister S (eds) EMSOFT. ACM, New York, pp 97–106. https://doi.org/10.1145/2038642.2038659
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems—specification. Springer, New York. https://doi.org/10.1007/978-1-4612-0931-7
Owicki SS, Lamport L (1982) Proving liveness properties of concurrent programs. ACM Trans Program Lang Syst 4(3):455–495. https://doi.org/10.1145/357172.357178
Prajna S, Jadbabaie A, Pappas GJ (2007) A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans Automat Control 52(8):1415–1428. https://doi.org/10.1109/TAC.2007.902736
Platzer A (2010) Differential-algebraic dynamic logic for differential-algebraic programs. J Log Comput 20(1):309–352. https://doi.org/10.1093/logcom/exn070
Platzer A The complete proof theory of hybrid systems. In: LICS [LIC12]. pp 541–550. https://doi.org/10.1109/LICS.2012.64
Platzer A Logics of dynamical systems. In: LICS [LIC12]. pp 13–24. https://doi.org/10.1109/LICS.2012.13
Platzer A (2017) A complete uniform substitution calculus for differential dynamic logic. J Autom Reason 59(2):219–265. https://doi.org/10.1007/s10817-016-9385-1
Platzer A (2017) Differential hybrid games. ACM Trans Comput Log 18(3):19:1–19:44. https://doi.org/10.1145/3091123
Platzer A (2018) Logical foundations of cyber-physical systems. Springer, Cham. https://doi.org/10.1007/978-3-319-63588-0
Papachristodoulou A, Prajna S (2002) On the construction of Lyapunov functions using the sum of squares decomposition. In: CDC, vol 3. IEEE, pp 3482–3487. https://doi.org/10.1109/CDC.2002.1184414
Platzer A, Quesel J-D (2008) KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando A, Baumgartner P, Dowek G (eds) IJCAR, volume 5195 of LNCS. Springer, pp 171–178. https://doi.org/10.1007/978-3-540-71070-7_15
Prajna S, Rantzer A (2005) Primal-dual tests for safety and reachability. In: Morari M, Thiele L (eds) HSCC, volume 3414 of LNCS. Springer, Heidelberg, pp 542–556. https://doi.org/10.1007/978-3-540-31954-2_35
Prajna S, Rantzer A (2007) Convex programs for temporal verification of nonlinear dynamical systems. SIAM J Control Optim 46(3):999–1021. https://doi.org/10.1137/050645178
Platzer A, Tan YK (2020) Differential equation invariance axiomatization. J ACM 67(1). https://doi.org/10.1145/3380825
Podelski A, Wagner S (2006) Model checking of hybrid systems: from reachability towards stability. In: Hespanha JP, Tiwari A (eds) HSCC, volume 3927 of LNCS. Springer, Heidelberg, pp 507–521. https://doi.org/10.1007/11730637_38
Rönkkö M, Ravn AP, Sere K (2003) Hybrid action systems. Theor Comput Sci 290(1):937–973. https://doi.org/10.1016/S0304-3975(02)00547-9
Ratschan S, She Z (2010) Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM J Control Optim 48(7):4377–4394. https://doi.org/10.1137/090749955
Rudin, W.: Principles of mathematical analysis, 3rd edn. McGraw-Hill, New York (1976)
Sogokon A, Jackson PB (2015) Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In Bjørner N, de Boer FS (eds) FM, volume 9109 of LNCS. Springer, Cham, pp 514–531. https://doi.org/10.1007/978-3-319-19249-9_32
Sogokon A, Jackson PB, Johnson TT (2019) Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants. J Autom Reason 63(4):1005–1029. https://doi.org/10.1007/s10817-018-9497-x
Sogokon A (2016) Direct methods for deductive verification of temporal properties in continuous dynamical systems. PhD thesis, Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh
Tan YK, Platzer A (2019) An axiomatic approach to liveness for differential equations. In: ter Beek MH, McIver A, Oliveira JN (eds) FM, volume 11800 of LNCS. Springer, Cham, pp 371–388. https://doi.org/10.1007/978-3-030-30942-8_23
Taly A, Tiwari A (2010) Switching logic synthesis for reachability. In: Carloni LP, Tripakis S (eds) EMSOFT. ACM, New York, pp 19–28. https://doi.org/10.1145/1879021.1879025
Walter W (1998) Ordinary differential equations. Springer, New York. https://doi.org/10.1007/978-1-4612-0601-9
Wang S, Zhan N, Zou L (2015) An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler MJ, Conchon S, Zaïdi F (eds) ICFEM, volume 9407 of LNCS. Springer, Cham, pp 382–399. https://doi.org/10.1007/978-3-319-25423-4_25
Zhang J, Johansson KH, Lygeros J, Sastry S (2001) Zeno hybrid systems. Int J Robust Nonlinear Control 11(5):435–451. https://doi.org/10.1002/rnc.592
Funding
The authors thank the guest editors for handling this article and the anonymous reviewers for their insightful comments and feedback. The authors also thank members of the Logical Systems Lab at Carnegie Mellon University for their feedback on the KeYmaera X implementation, and Katherine Cordwell, Frank Pfenning, Andrew Sogokon, and the FM'19 anonymous reviewers for their feedback on the earlier conference version. 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.
Author information
Authors and Affiliations
Corresponding author
Additional information
Annabelle McIver, Maurice ter Beek and Cliff Jones
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Tan, Y.K., Platzer, A. An axiomatic approach to existence and liveness for differential equations. Form Asp Comp 33, 461–518 (2021). https://doi.org/10.1007/s00165-020-00525-0
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-020-00525-0