Abstract
In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as the satisfiability of a second-order logical formula, asking whether there exists a function satisfying a desired specification (stability) for all possible initial conditions of the model. We synthesise Lyapunov functions for linear, non-linear (polynomial), and for parametric models. For non-linear models, the algorithm also determines a region of validity for the Lyapunov function. We exploit an inductive framework to synthesise Lyapunov functions, starting from parametric templates. The inductive framework comprises two elements: a learner proposes a Lyapunov function, and a verifier checks its validity - its lack is expressed via a counterexample (a point over the state space), for further use by the learner. Whilst the verifier uses the SMT solver Z3, thus ensuring the overall soundness of the procedure, we examine two alternatives for the learner: a numerical approach based on the optimisation tool Gurobi, and a sound approach based again on Z3. The overall technique is evaluated over a broad set of benchmarks, which shows that this methodology not only scales to 10-dimensional models within reasonable computational time, but also offers a novel soundness proof for the generated Lyapunov functions and their domains of validity.
Chapter PDF
Similar content being viewed by others
References
P. Giesl and S. Hafstein, “Review on Computational Methods for Lyapunov Functions," Discrete and Continuous Dynamical Systems-Series B, vol. 20, no. 8, pp. 2291–2331, 2015.
C. M. Kellett, “Classical Converse Theorems in Lyapunov’s Second Method”, Discrete Continuous Dyn. Syst. Series B, vol. 20, no. 8, pp. 2333–2360, 2015.
A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat, “Combinatorial Sketching for Finite Programs," ACM Sigplan Notices, vol. 41, no. 11, pp. 404–415, 2006.
C. David and D. Kroening, “Program Synthesis: Challenges and Opportunities," Phil. Trans. R. Soc. A, vol. 375, no. 2104, p. 20150403, 2017.
A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, E. Polgreen, and D. Kroening, “Automated formal synthesis of digital controllers for state-space physical plants,” in Proceedings of CAV, LNCS 10426, 2017, pp. 462–482.
A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening, and E. Polgreen, “Automated formal synthesis of provably safe digital controllers for continuous plants," Acta Informatica, 2020.
H. Ravanbakhsh and S. Sankaranarayanan, “Counter-example guided synthesis of control lyapunov functions for switched systems," in IEEE Control and Decision Conference (CDC), 2015, pp. 4232–4239.
—, “Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework," in ACM/IEEE Conference on Embedded Software (EMSOFT), 2016, pp. 8:1–8:10.
D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of View, ser. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin Heidelberg, 2016.
Gurobi Optimization, LLC, “Gurobi Optimizer Reference Manual," 2018. [Online]. Available: http://www.gurobi.com
L. De Moura and N. Bjørner, “Z3: An Efficient SMT solver," in International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340.
R. Kalman and J. Bertram, “Control System Analysis and Design via the “Second Method” of Lyapunov: Part I Continuous-time Systems," Trans. AMSE Series D J. Basic Eng., vol. 82, no. 2, pp. 371–393, 1960.
N. N. Krasovskii, Stability of Motion: Applications of Lyapunov’s Second Method to Differential Systems and Equations With Delay. Stanford Univ. Press, 1963.
J. LaSalle and S. Lefschetz, Stability by Liapunov’s Direct Method With Applications. Academic Press, 1961.
V. I. Zubov, Methods of A. M. Lyapunov and Their Application. Noordhoff, 1964.
R. Brayton and C. Tong, “Stability of Dynamical Systems: A Constructive Approach," IEEE Transactions on Circuits and Systems, vol. 26, no. 4, pp. 224–234, 1979.
P. A. Parrilo, “Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization," Ph.D. dissertation, California Institute of Technology, 2000.
A. Papachristodoulou and S. Prajna, “On the Construction of Lyapunov Functions using the Sum of Squares Decomposition," in Proceedings of the 41st IEEE Conference on Decision and Control, 2002, vol. 3. IEEE, 2002, pp. 3482–3487.
S. Prajna, A. Papachristodoulou, and P. A. Parrilo, “SOSTOOLS: Sum of squares Optimization Toolbox for MATLAB-User’s Guide," Control and Dynamical Systems, California Institute of Technology, Pasadena, CA, vol. 91125, 2004.
A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. Parrilo, “SOSTOOLS Version 3.03. Sum of Squares Optimization Toolbox for MATLAB," 2018.
R. Geiselhart, R. H. Gielen, M. Lazar, and F. R. Wirth, “An Alternative Converse Lyapunov Theorem for Discrete-time Systems," Syst. Control Lett., vol. 70, pp. 49–59, 2014.
S. F. Hafstein, “An Algorithm for Constructing Lyapunov Functions," Electron. J. Differ. Equ. Monograph, vol. 8, 207.
S. Sankaranarayanan, X. Chen, and E. Abraham, “Lyapunov Function Synthesis using Handelman Representations," IFAC Proceedings Volumes, vol. 46, no. 23, pp. 576–581, 2013.
J. Kapinski, J. V. Deshmukh, S. Sankaranarayanan, and N. Arechiga, “Simulation-guided Lyapunov Analysis for Hybrid Dynamical Systems," in Proceedings of the 17th international conference on Hybrid systems: computation and control. ACM, 2014, pp. 133–142.
S. Gao, S. Kong, and E. M. Clarke, “dReal: An SMT Solver for Nonlinear Theories over the Reals," in International Conference on Automated Deduction. Springer, 2013, pp. 208–214.
Wolfram Research Inc, “Mathematica, Version 12.0," 2019.
H. Ravanbakhsh and S. Sankaranarayanan, “Learning Control Lyapunov Functions from Counterexamples and Demonstrations," Autonomous Robots, pp. 1–33, 2018.
E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of model checking. Springer, 2018, vol. 10.
Microsoft Research, “The Z3 Theorem Prover," https://github.com/Z3Prover/z3, accessed: 2018–07-25.
Python Software Foundation, “Python Language Reference, version 2.7," http://www.python.org.
J. F. Sturm, “Using SeDuMi 1.02, a MATLAB Toolbox for Optimization over Symmetric Cones," Optimization methods and software, vol. 11, no. 1–4, pp. 625–653, 1999.
Y. Chang, N. Roohi, and S. Gao, “Neural Lyapunov Control," in NeurIPS, 2019, pp. 3240–3249.
Author information
Authors and Affiliations
Corresponding author
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
© 2020 The Author(s)
About this paper
Cite this paper
Ahmed, D., Peruffo, A., Abate, A. (2020). Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)