Abstract
Stability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of dL with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from dL’s axioms with dL’s ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on dL.
This research was sponsored by the AFOSR under grant number FA9550-16-1-0288.
The first author was supported by A*STAR, Singapore.
Chapter PDF
Similar content being viewed by others
References
Ahmed, D., Peruffo, A., Abate, A.: Automated and sound synthesis of Lyapunov functions with SMT solvers. In: Biere, A., Parker, D. (eds.) TACAS. LNCS, vol. 12078, pp. 97–114. Springer (2020). https://doi.org/10.1007/978-3-030-45190-5_6
Alur, R.: Principles of Cyber-Physical Systems. MIT Press (2015)
Ashbaugh, M.S., Chicone, C.C., Cushman, R.H.: The twisting tennis racket. Journal of Dynamics and Differential Equations 3, 67–85 (1991). https://doi.org/10.1007/BF01049489
Bochnak, J., Coste, M., Roy, M.F.: Real Algebraic Geometry. Springer, Heidelberg (1998). https://doi.org/10.1007/978-3-662-03718-8
Branicky, M.S.: Introduction to hybrid systems. In: Hristu-Varsakelis, D., Levine, W.S. (eds.) Handbook of Networked and Embedded Control Systems, pp. 91–116. Birkhäuser (2005). https://doi.org/10.1007/0-8176-4404-0_5
Chicone, C.: Ordinary Differential Equations with Applications. Springer, New York, second edn. (2006). https://doi.org/10.1007/0-387-35794-7
Cohen, C., Rouhling, D.: A formal proof in Coq of LaSalle’s invariance principle. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP. LNCS, vol. 10499, pp. 148–163. Springer (2017). https://doi.org/10.1007/978-3-319-66107-0_10
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_30
Forsman, K.: Construction of Lyapunov functions using Gröbner bases. In: CDC. vol. 1, pp. 798–799. IEEE (1991). https://doi.org/10.1109/CDC.1991.261424
Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: Tactical theorem proving for hybrid systems. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP. LNCS, vol. 10499, pp. 207–224. Springer (2017). https://doi.org/10.1007/978-3-319-66107-0_14
Fulton, N., Mitsch, S., Quesel, J., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE. LNCS, vol. 9195, pp. 527–538. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_36
Gao, S., Kapinski, J., Deshmukh, J.V., Roohi, N., Solar-Lezama, A., Aréchiga, N., Kong, S.: Numerically-robust inductive proof rules for continuous dynamical systems. In: Dillig, I., Tasiran, S. (eds.) CAV. LNCS, vol. 11562, pp. 137–154. Springer (2019). https://doi.org/10.1007/978-3-030-25543-5_9
Goebel, R., Sanfelice, R.G., Teel, A.R.: Hybrid Dynamical Systems: Modeling, Stability, and Robustness. Princeton University Press (2012)
Haddad, W.M., Chellaboina, V.: Nonlinear Dynamical Systems and Control: A Lyapunov-Based Approach. Princeton University Press (2008)
Hirsch, M.W.: The dynamical systems approach to differential equations. Bull. Amer. Math. Soc. (N.S.) 11(1), 1–64 (07 1984)
Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP. LNCS, vol. 7998, pp. 279–294. Springer (2013). https://doi.org/10.1007/978-3-642-39634-2_21
Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Aréchiga, N.: Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: Fränzle, M., Lygeros, J. (eds.) HSCC. pp. 133–142. ACM (2014). https://doi.org/10.1145/2562059.2562139
Khalil, H.K.: Nonlinear systems. Macmillan Publishing Company, New York (1992)
Liapounoff, A.: Probléme général de la stabilité du mouvement. Annales de la Faculté des sciences de Toulouse : Mathématiques 9, 203–474 (1907)
Liberzon, D.: Switching in Systems and Control. Systems & Control: Foundations & Applications, Birkhäuser (2003). https://doi.org/10.1007/978-1-4612-0017-8
Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems. Math. Comput. Sci. 6(4), 395–408 (2012). https://doi.org/10.1007/s11786-012-0133-6
Nguyen, L.V., Kapinski, J., Jin, X., Deshmukh, J.V., Johnson, T.T.: Hyperproperties of real-valued signals. In: Talpin, J., Derler, P., Schneider, K. (eds.) MEMOCODE. pp. 104–113. ACM (2017). https://doi.org/10.1145/3127041.3127058
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
Parrilo, P.A.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. Ph.D. thesis, California Institute of Technology (2000)
Platzer, A.: The complete proof theory of hybrid systems. In: LICS. pp. 541–550. IEEE Computer Society (2012). https://doi.org/10.1109/LICS.2012.64
Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reasoning 59(2), 219–265 (2017). https://doi.org/10.1007/s10817-016-9385-1
Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63588-0
Platzer, A., Tan, Y.K.: Differential equation invariance axiomatization. J. ACM 67(1) (2020). https://doi.org/10.1145/3380825
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 (2006). https://doi.org/10.1007/11730637_38
Poincaré, H.: Les méthodes nouvelles de la mécanique céleste. Gauthier-Villars, Paris (1892–1899)
Rouche, N., Habets, P., Laloy, M.: Stability Theory by Liapunov’s Direct Method. Springer, New York (1977). https://doi.org/10.1007/978-1-4684-9362-7
Rouhling, D.: A formal proof in Coq of a control function for the inverted pendulum. In: Andronick, J., Felty, A.P. (eds.) CPP. pp. 28–41. ACM (2018). https://doi.org/10.1145/3167101
Sankaranarayanan, S., Chen, X., Ábrahám, E.: Lyapunov function synthesis using Handelman representations. In: Tarbouriech, S., Krstic, M. (eds.) NOLCOS. pp. 576–581. IFAC (2013). https://doi.org/10.3182/20130904-3-FR-2041.00198
Strogatz, S.H.: Nonlinear Dynamics and Chaos: With Applications to Physics, Biology, Chemistry, and Engineering. Westview Press, Boulder, CO, second edn. (2015)
Tan, Y.K., Platzer, A.: Deductive stability proofs for ordinary differential equations. CoRR abs/2010.13096 (2020), https://arxiv.org/abs/2010.13096
Tan, Y.K., Platzer, A.: An axiomatic approach to existence and liveness for differential equations. Formal Aspects Comput. (to appear). https://doi.org/10.1007/s00165-020-00525-0
Topcu, U., Packard, A.K., Seiler, P.J.: Local stability analysis using simulations and sum-of-squares programming. Autom. 44(10), 2669–2675 (2008). https://doi.org/10.1016/j.automatica.2008.03.010
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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 license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license 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.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Tan, Y.K., Platzer, A. (2021). Deductive Stability Proofs for Ordinary Differential Equations. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)