Synthesis of Lyapunov Functions using Formal Verification
Systems and Control
2021-12-06 v1 Systems and Control
Abstract
Recent employments of SMT solvers within the Lyapunov function synthesis provided effective tools for automated construction of Lyapunov functions alongside with sound computer-assisted certificates. The main benefit of the suggested approach is the formal correctness and elimination of the numerical uncertainty. In the present work, we extend the SMT-based synthesis approach for wider classes of continuous and discrete-time systems. Additionally, we address constructions of Lyapunov functions for state-dependent switching systems. We illustrate our approach by means of various examples from the control systems literature.
Cite
@article{arxiv.2112.01835,
title = {Synthesis of Lyapunov Functions using Formal Verification},
author = {Lukas Munser and Grigory Devadze and Stefan Streif},
journal= {arXiv preprint arXiv:2112.01835},
year = {2021}
}