论文标题
通过平方证书和建设性分析的计算机辅助证明Lyapunov稳定性
Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis
论文作者
论文摘要
我们提供了一种计算机辅助的方法，以确保给定的连续或离散时间多项式系统（渐近）稳定。我们的框架依靠建设性分析以及正式认证的Squares Lyapunov功能。关键步骤是在证明助理MinLog内部正式的。我们用控制系统文献发布的各种示例来说明我们的方法。
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.
