Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis
Optimization and Control
2024-08-02 v2 Logic in Computer Science
Abstract
We provide a computer-assisted approach to ensure that a given continuous or discrete-time polynomial system is (asymptotically) stable. Our framework relies on constructive analysis together with formally certified sums of squares Lyapunov functions. The crucial steps are formalized within of the proof assistant Minlog. We illustrate our approach with various examples issued from the control system literature.
Keywords
Cite
@article{arxiv.2006.09884,
title = {Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis},
author = {Grigory Devadze and Victor Magron and Stefan Streif},
journal= {arXiv preprint arXiv:2006.09884},
year = {2024}
}