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

2020/06/17 by Devadze, Grigory, Magron, Victor, Streif, Stefan
#FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Optimization and Control (math.OC)

paper · doi:10.48550/arxiv.2006.09884

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.

Related

• A Converse Sum of Squares Lyapunov Result with a Degree Bound
• A Sum-of-Squares approach to the Stability and Control of Interconnected\n Systems using Vector Lyapunov Functions
• Stability of Polynomial Differential Equations: Complexity and Converse\n Lyapunov Questions
• Initial Application of SONC to Lyapunov Stability of Dynamical Systems
• SOS Construction of Compatible Control Lyapunov and Barrier Functions