An Axiomatic Approach to Liveness for Differential Equations

  • Yong Kiam TanEmail author
  • André PlatzerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


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.


Differential 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.


  1. 1.
    Abate, A., D’Innocenzo, A., Benedetto, M.D.D., Sastry, S.: Understanding deadlock and livelock behaviors in hybrid control systems. Nonlinear Anal. Hybrid Syst. 3(2), 150–162 (2009). Scholar
  2. 2.
    Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)Google Scholar
  3. 3.
    Bochnak, J., Coste, M., Roy, M.F.: Real Algebraic Geometry. Springer, Heidelberg (1998). Scholar
  4. 4.
    Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). Scholar
  5. 5.
    Chicone, C.: Ordinary Differential Equations with Applications, 2nd edn. Springer, New York (2006). Scholar
  6. 6.
    Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1047–1110. Springer, Cham (2018). Scholar
  7. 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).
  8. 8.
    Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). Scholar
  9. 9.
    Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS. LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014). Scholar
  10. 10.
    Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Frehse, G., Mitra, S. (eds.) HSCC, pp. 1–10. ACM, New York (2017). Scholar
  11. 11.
    Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 97–106. ACM, New York (2011). Scholar
  12. 12.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992). Scholar
  13. 13.
    Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982). Scholar
  14. 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).
  15. 15.
    Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010). Scholar
  16. 16.
    Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13–24. IEEE (2012).
  17. 17.
    Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. 59(2), 219–265 (2017). Scholar
  18. 18.
    Platzer, A.: Differential hybrid games. ACM Trans. Comput. Log. 18(3), 19:1–19:44 (2017). Scholar
  19. 19.
    Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). Scholar
  20. 20.
    Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Dawar, A., Grädel, E. (eds.) LICS, pp. 819–828. ACM, New York (2018). Scholar
  21. 21.
    Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC. LNCS, vol. 3927, pp. 507–521. Springer, Heidelberg (2006). Scholar
  22. 22.
    Prajna, S., Rantzer, A.: Primal-dual tests for safety and reachability. In: Morari, M., Thiele, L. (eds.) HSCC. LNCS, vol. 3414, pp. 542–556. Springer, Heidelberg (2005). Scholar
  23. 23.
    Prajna, S., Rantzer, A.: Convex programs for temporal verification of nonlinear dynamical systems. SIAM J. Control Optim. 46(3), 999–1021 (2007). Scholar
  24. 24.
    Ratschan, S., She, Z.: 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 (2010). Scholar
  25. 25.
    Sogokon, A., Jackson, P.B.: Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In: Bjørner, N., de Boer, F.S. (eds.) FM. LNCS, vol. 9109, pp. 514–531. Springer, Cham (2015). Scholar
  26. 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).
  27. 27.
    Taly, A., Tiwari, A.: Switching logic synthesis for reachability. In: Carloni, L.P., Tripakis, S. (eds.) EMSOFT, pp. 19–28. ACM, New York (2010). Scholar
  28. 28.
    Tan, Y.K., Platzer, A.: An axiomatic approach to liveness for differential equations. CoRR abs/1904.07984 (2019)Google Scholar
  29. 29.
    Walter, W.: Ordinary Differential Equations. Springer, New York (1998). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations