Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis

TL;DR

This paper introduces a computer-assisted method using formalized sums of squares and constructive analysis within Minlog to verify the stability of polynomial systems, enhancing rigor in control theory proofs.

Contribution

It presents a novel formalized framework combining constructive analysis and certified sums of squares for Lyapunov stability verification.

Findings

Successfully verified stability of multiple control systems

Demonstrated formal certification within Minlog proof assistant

Enhanced rigor and reliability of stability proofs

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.