Advertisement

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)

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.

Keywords

Differential equations Liveness Differential dynamic logic 

Notes

Acknowledgments

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.

References

  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).  https://doi.org/10.1016/j.nahs.2008.12.005MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-662-03718-8CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-39799-8_18CrossRefGoogle Scholar
  5. 5.
    Chicone, C.: Ordinary Differential Equations with Applications, 2nd edn. Springer, New York (2006).  https://doi.org/10.1007/0-387-35794-7CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-319-10575-8_30CrossRefzbMATHGoogle 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).  https://doi.org/10.1145/2185632.2185652
  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).  https://doi.org/10.1007/978-3-642-22110-1_30CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-54862-8_19CrossRefGoogle 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).  https://doi.org/10.1145/3049797.3049811CrossRefGoogle 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).  https://doi.org/10.1145/2038642.2038659CrossRefGoogle Scholar
  12. 12.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992).  https://doi.org/10.1007/978-1-4612-0931-7CrossRefzbMATHGoogle Scholar
  13. 13.
    Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982).  https://doi.org/10.1145/357172.357178CrossRefzbMATHGoogle 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).  https://doi.org/10.1109/CDC.2002.1184414
  15. 15.
    Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010).  https://doi.org/10.1093/logcom/exn070MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13–24. IEEE (2012).  https://doi.org/10.1109/LICS.2012.13
  17. 17.
    Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. 59(2), 219–265 (2017).  https://doi.org/10.1007/s10817-016-9385-1MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Platzer, A.: Differential hybrid games. ACM Trans. Comput. Log. 18(3), 19:1–19:44 (2017).  https://doi.org/10.1145/3091123MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-63588-0CrossRefzbMATHGoogle 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).  https://doi.org/10.1145/3209108.3209147CrossRefGoogle 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).  https://doi.org/10.1007/11730637_38CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-31954-2_35CrossRefGoogle 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).  https://doi.org/10.1137/050645178MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1137/090749955MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-319-19249-9_32CrossRefGoogle 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).  https://doi.org/10.1007/s10817-018-9497-x
  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).  https://doi.org/10.1145/1879021.1879025CrossRefGoogle 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).  https://doi.org/10.1007/978-1-4612-0601-9CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations