AI 中文总结
该研究在精益中引入开源库用于机器验证控制理论，给出李雅普诺夫稳定性理论和小增益定理的形式化，前者用邻域滤波器涵盖多种系统，后者通过新方式证明，还介绍了库架构等及未来计划。
AI 中文摘要
我们在交互式证明助手精益中引入了一个用于机器验证控制理论的开源库，为网络物理系统的验证奠定基础。作为代表性定理，我们给出了李雅普诺夫稳定性理论和小增益定理的形式化。首先，用于形式化李雅普诺夫稳定性的机制，即邻域滤波器，使我们能够陈述一个涵盖点和集合且适用于连续、离散和混合系统的李雅普诺夫定理。其次，小增益定理是通过将输入 - 输出系统表述为关系而无需通常的适定性假设来证明的。然后展示了这些定理在精益中的形式化。最后讨论了库架构，并提及了库中形式化的其他一些系统理论结果以及未来计划。
英文摘要
We introduce an open-source library for machine-checked control theory in the interactive proof assistant Lean to lay foundations for the verification of cyber-physical systems. To this end, as representative theorems, we present formalizations of Lyapunov stability theory and the small-gain theorem. First, the machinery employed for formalizing Lyapunov stability, i.e., neighborhood filters, allows stating a Lyapunov theorem that covers both points and sets and applies to continuous, discrete, and hybrid systems. Second, the small-gain theorem is proved via stating input-output systems as relations without the usual well-posedness assumption. The Lean formalization of each of these theorems is then presented. We conclude by discussing the library architecture and mentioning some of the other system theoretic results that are formalized in the library along with future plans.
Comments15 pages, 1 figure
