首页|Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis
Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis
扫码查看
点击上方二维码区域，可以放大扫码查看
原文链接
NETL
NSTL
Springer Nature
Abstract 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 Minlog\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\texttt {Minlog}$$\end{document}. We illustrate our approach with an example issued from the control system literature.
NETL
NSTL
Springer Nature
