Scholarlink

<p>We provide a computer-assisted approach to ensure that a given 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 the proof assistant <InlineEquation ID="IEq1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10817_2024_9717_Article_IEq1.gif" Format="GIF" Height="16" Rendition="HTML" Resolution="72" Type="Linedraw" Width="54" /> </InlineMediaObject> <EquationSource Format="TEX">\(\texttt {Minlog}\)</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="monospace">Minlog</mi> </math></EquationSource> </InlineEquation>. We illustrate our approach with an example issued from the control system literature.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年1月25日

查看全文
  • Grigory Devadze,
  • Victor Magron,
  • Stefan Streif

摘要

We provide a computer-assisted approach to ensure that a given 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 the proof assistant \(\texttt {Minlog}\) Minlog . We illustrate our approach with an example issued from the control system literature.