A formal proof in Coq of Lasalle’s invariance principle. (English) Zbl 1484.68315
Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 148-163 (2017).
Summary: Stability analysis of dynamical systems plays an important role in the study of control techniques. LaSalle’s invariance principle is a result about the asymptotic stability of the solutions to a nonlinear system of differential equations and several extensions of this principle have been designed to fit different particular kinds of system. In this paper we present a formalization, in the Coq proof assistant, of a slightly improved version of the original principle. This is a step towards a formal verification of dynamical systems.
For the entire collection see [Zbl 1369.68009].
For the entire collection see [Zbl 1369.68009].
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 34D20 | Stability of solutions to ordinary differential equations |
References:
| [1] | Barkana, I., Defending the beauty of the Invariance Principle, Int. J. Control, 87, 1, 186-206 (2014) · Zbl 1317.93229 · doi:10.1080/00207179.2013.826385 |
| [2] | Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Interactive Theorem Proving (2013), Heidelberg: Springer, Heidelberg · Zbl 1268.68006 · doi:10.1007/978-3-642-39634-2 |
| [3] | Boldo, S.; Lelay, C.; Melquiond, G., Coquelicot: A User-Friendly Library of Real Analysis for Coq, Math. Comput. Sci., 9, 1, 41-62 (2015) · Zbl 1322.68176 · doi:10.1007/s11786-014-0181-1 |
| [4] | Cano, G.: Interaction entre algèbre linéaire et analyse en formalisation des mathématiques. (Interaction between linear algebra and analysis in formal mathematics). Ph.D. thesis, University of Nice Sophia Antipolis, France (2014). https://tel.archives-ouvertes.fr/tel-00986283 |
| [5] | Chan, M., Ricketts, D., Lerner, S., Malecha, G.: Formal Verification of Stability Properties of Cyber-Physical Systems, January 2016 |
| [6] | Chellaboina, V.; Leonessa, A.; Haddad, WM, Generalized Lyapunov and invariant set theorems for nonlinear dynamical systems, Syst. Control Lett., 38, 4-5, 289-295 (1999) · Zbl 0985.93053 · doi:10.1016/S0167-6911(99)00076-6 |
| [7] | Darmochwał, A., Compact Spaces, Formaliz. Math., 1, 2, 383-386 (1990) |
| [8] | Fischer, NR; Kamalapurkar, R.; Dixon, WE, LaSalle-Yoshizawa Corollaries for Nonsmooth Systems, IEEE Trans. Automat. Control, 58, 9, 2333-2338 (2013) · Zbl 1369.34023 · doi:10.1109/TAC.2013.2246900 |
| [9] | Gonthier, G., Formal Proof - The Four-Color Theorem, Notices AMS, 55, 11, 1382-1393 (2008) · Zbl 1195.05026 |
| [10] | Gonthier, G., et al.: A Machine-Checked Proof of the Odd Order Theorem. In: Blazy et al. [2], pp. 163-179 (2013). doi:doi:10.1007/978-3-642-39634-2_14 · Zbl 1317.68211 |
| [11] | Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2015). https://hal.inria.fr/inria-00258384 |
| [12] | Herencia-Zapana, H.; Jobredeaux, R.; Owre, S.; Garoche, P-L; Feron, E.; Perez, G.; Ascariz, P.; Goodloe, AE; Person, S., PVS linear algebra libraries for verification of control software algorithms in C/ACSL, NASA Formal Methods, 147-161 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-28891-3_15 |
| [13] | Hölzl, J., Immler, F., Huffman, B.: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. In: Blazy et al. [2], pp. 279-294 (2013). doi:doi:10.1007/978-3-642-39634-2_21 · Zbl 1317.68213 |
| [14] | Khalil, H.: Nonlinear Systems. Pearson Education, Prentice Hall (2002). https://books.google.fr/books?id=t_d1QgAACAAJ |
| [15] | LaSalle, J., Some Extensions of Liapunov’s Second Method, IRE Trans. Circ. Theory, 7, 4, 520-527 (1960) · doi:10.1109/TCT.1960.1086720 |
| [16] | Lester, D.R.: Topology in PVS: Continuous Mathematics with Applications. In: Proceedings of the Second Workshop on Automated Formal Methods, AFM 2007, pp. 11-20. ACM, New York (2007). doi:10.1145/1345169.1345171 |
| [17] | Liapounoff, A.: Problème général de la stabilité du mouvement. In: Annales de la Faculté des sciences de Toulouse: Mathématiques, vol. 9, pp. 203-474 (1907). http://eudml.org/doc/72801 · JFM 38.0738.07 |
| [18] | Lozano, R.; Fantoni, I.; Block, D., Stabilization of the inverted pendulum around its homoclinic orbit, Syst. Control Lett., 40, 3, 197-204 (2000) · Zbl 0985.93026 · doi:10.1016/S0167-6911(00)00025-6 |
| [19] | Mancilla-Aguilar, JL; García, RA, An extension of LaSalle’s invariance principle for switched systems, Syst. Control Lett., 55, 5, 376-384 (2006) · Zbl 1129.93445 · doi:10.1016/j.sysconle.2005.07.009 |
| [20] | Mayero, M.: Formalisation et automatisation de preuves en analyses réelle et numérique. Ph.D. thesis, Université Paris VI (décembre 2001) |
| [21] | Mitra, S.; Chandy, KM; Mohamed, OA; Muñoz, C.; Tahar, S., A Formalized Theory for Verifying Stability and Convergence of Automata in PVS, Theorem Proving in Higher Order Logics, 230-245 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68394 · doi:10.1007/978-3-540-71067-7_20 |
| [22] | Padlewska, B.; Darmochwał, A., Topological Spaces and Continuous Functions, Formaliz. Math., 1, 1, 223-230 (1990) |
| [23] | The Coq Development Team: The Coq proof assistant reference manual, version 8.6. (2016). http://coq.inria.fr |
| [24] | Wilansky, A.: Topology for Analysis. Dover Books on Mathematics. Dover Publications, New York (2008). http://cds.cern.ch/record/2222525 · Zbl 0229.54001 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
