基于平方和证书与构造性分析的 Lyapunov 稳定性计算机辅助证明
最优化与控制
2024-08-02 v2 计算机科学中的逻辑
摘要
我们提供了一种计算机辅助方法，以确保给定的连续或离散时间多项式系统是（渐近）稳定的。我们的框架依赖于构造性分析以及形式化认证的平方和 Lyapunov 函数。关键步骤在证明辅助工具 Minlog 中形式化。我们用控制系统文献中的各种例子说明了我们的方法。
引用
@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}
}