Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification
University of Waterloo（滑铁卢大学）
本文研究用物理信息神经网络求解李雅普诺夫函数，通过将李雅普诺夫条件编码为PDE并利用Zubov方程训练，结合SMT求解器进行形式化验证，在多个非线性示例上优于传统SOS/SDP方法。
2025-01-10 cs.LG cs.SY eess.SY
Optimization of Lyapunov Invariants in Verification of Software Systems (Extended Version)
Laboratory for Information and Decision Systems (LIDS), Massachusetts Institute of Technology（麻省理工学院信息与决策系统实验室）；School of Aerospace Engineering, Georgia Institute of Technology（佐治亚理工学院航空航天学院）
提出一种基于控制理论的框架，通过构造Lyapunov不变量并求解凸优化问题，验证数值软件系统的安全性和性能规范。
2011-08-29 cs.SE cs.SY eess.SY
Stochastic Stability Analysis of Discrete Time System Using Lyapunov Measure
Iowa State University（爱荷华州立大学）
本文研究了随机非线性离散时间系统的稳定性问题，提出基于线性转移算子的李雅普诺夫度量作为稳定性验证工具，并建立了李雅普诺夫函数与度量之间的联系，通过双算子性质展示其对偶性，提出有限维近似方法和粗随机稳定性概念。
2016-03-08 cs.SY eess.SY math.DS
Stability Verification for Switched Systems using Neural Multiple Lyapunov Functions
School of Automation and Intelligent Sensing, Shanghai 200240, China（自动化与智能感知学院）
本文提出神经多Lyapunov函数，结合理论保证与计算效率，用于状态依赖切换条件下的切换系统稳定性分析。
2026-01-02 cs.SY eess.SY
Convex synthesis and verification of control-Lyapunov and barrier functions with input constraints
Toyota Research Institute（丰田研究院）
控制李雅普诺夫函数（CLF）和控制障碍函数（CBF）是广泛使用的工具，综合控制器的稳定性和安全性的约束。与在线优化相结合，它们提供了满足输入约束的稳定控制动作，并避免了状态空间的不安全区域。设计具有严格性能保证的CLF和CBF在计算上具有挑战性。为了证明控制行为的存在性，现有技术不仅设计CLF/CBF，而且设计标称控制器。这可能使合成任务更昂贵，并且性能估计更保守。在这项工作中，我们使用平方和条件，可以直接使用凸优化证明多项式CLF/CBF的特征。这产生了一个CLF和CBF合成技术，不依赖于一个标称控制器。然后，我们提出的算法迭代扩大估计的稳定和安全的区域。我们证明了我们的算法上的2D玩具系统，一个钟摆和四旋翼。
2022-10-02 cs.RO cs.SY eess.SY
Region of Attraction Estimate Learning and Verification for Nonlinear Systems using Neural-Network-based Lyapunov Functions
Mitsubishi Electric R&D Centre Europe（三菱电机欧洲研发中心）
针对非线性系统吸引域估计传统方法保守性强、高维场景构建难的问题，提出结合复合神经网络李雅普诺夫函数、齐次损失训练与SMT形式化验证的数据驱动框架，在基准系统上验证了其低保守性与可验证性。
2025-11-14 cs.SY eess.SY math.DS
Formally Verified Physics-Informed Neural Control Lyapunov Functions
University of Waterloo（滑铁卢大学）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
本文提出了一种基于物理信息的神经网络控制李雅普诺夫函数学习与形式验证方法，通过变换后的哈密尔顿-雅可比-贝尔曼方程实现对非线性系统可控零集的描述，并通过数值实验验证其有效性。
2024-09-30 cs.LG cs.SY eess.SY
Analytical Lyapunov Function Discovery: An RL-based Generative Approach
Department of Electrical and Computer Engineering, UC San Diego, La Jolla, United States（加州大学圣地亚哥分校电子与计算机工程系）；Swiss Federal Institute of Technology in Lausanne（洛桑联邦理工学院）
本文提出一种基于transformer和强化学习的端到端框架，通过训练器生成候选解析李雅普诺夫函数并用证伪器验证改进，成功为高维及非多项式系统发现局部李雅普诺夫函数，提升了可解释性和验证效率。
2025-06-04 cs.AI cs.LG cs.SC
Verification and Synthesis of Compatible Control Lyapunov and Control Barrier Functions
Washington University in St. Louis（圣路易斯华盛顿大学）；McKelvey School of Engineering（麦凯维工程学院）；Toyota Research Institute（丰田研究所）
针对现有CBF与CLF分别验证综合易导致控制器失效、现有兼容方法依赖标称控制器仅为充分条件的问题，提出无标称控制器的兼容验证充要条件与平方和规划验证框架及综合方法，可扩大兼容区域，经非线性算例和3D四旋翼验证具可扩展性，代码开源。
2024-09-14 cs.RO cs.SY eess.SY
Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light
本文提出利用多项式方法研究 switched 系统稳定性，基于伯恩斯坦插值法构建 Lyapunov 函数，并通过 HOL Light 验证其形式正确性。
2014-10-15 cs.SY eess.SY
Scalable Formal Verification of Incremental Stability in Large-Scale Systems Using Graph Neural Networks
Indian Institute of Science, Bengaluru（印度科学研究所）
本文提出利用图神经网络进行大规模系统增量稳定性验证，通过构造局部李雅普诺夫函数并结合利普希茨界保证形式正确性。
2025-12-08 cs.SY eess.SY
Learning fixed-complexity polyhedral Lyapunov functions from counterexamples
研究了混合线性系的多面体李雅普诺夫函数的综合问题。这样的函数被定义为凸分段线性函数，具有有限数量的片段。我们首先证明了对于给定的混合线性系，判断是否存在$m$片多面体李雅普诺夫函数是NP难的。然后，我们提出了一个反例引导算法来解决这个问题。该算法交替选择一个候选多面体函数的基础上的一个有限集的反例，并验证候选是否满足李雅普诺夫条件。如果验证失败，我们会找到一个新的反例添加到我们的集合中。我们证明，如果算法终止，它发现一个有效的李雅普诺夫函数或得出结论，没有这样的李雅普诺夫函数存在。然而，我们的初始算法可以是非终止的。我们修改我们的算法，提供一个终止版本的基础上所谓的切割平面参数从非光滑最优化。我们证明了我们的算法的数值例子。
2022-09-14 cs.SY eess.SY math.OC
Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control
University of California, Riverside（加州大学河滨分校）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；University of California, Los Angeles（加州大学洛杉矶分校）
本文提出CT-BaB框架，通过动态训练数据集和自适应分割技术，提升神经控制器在区域吸引域内的认证保证，减少训练与验证时间差异，实现更高效的验证和更大的吸引域。
2026-04-06 cs.AI cs.LG cs.RO
Deep Reinforcement Learning Graphs: Feedback Motion Planning via Neural Lyapunov Verification
本文提出一种基于深度强化学习控制器图与神经网络的反馈运动规划算法，通过树结构和图结构两种连接方式分别实现点到点和空间到空间控制，并在一阶动态系统上验证了其有效性。
2023-11-29 cs.RO cs.SY eess.SY
Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems
State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）
本文通过引入高阶Lie导数推广标准Lyapunov函数为松弛Lyapunov函数，并提出一种完整方法自动发现多项式动力系统的所有多项式松弛Lyapunov函数。
2011-03-17 cs.SY eess.SY math.DS
Learning Robust Control Lyapunov Functions through Lipschitz Neural Networks
New York University（纽约大学）
提出学习鲁棒控制李雅普诺夫函数和稳定控制器的新框架，利用李普希茨神经网络联合学习，建立神经网络高阶导数边界并引入算法加速验证，通过模拟验证方法。
2026-10-08 cs.SY eess.SY
Contributions to Semialgebraic-Set-Based Stability Verification of Dynamical Systems with Neural-Network-Based Controllers
ETH Zurich（苏黎世联邦理工学院）
针对含神经网络控制器的动力系统闭环稳定性验证难题，本文从半代数激活函数、兼容递归平衡网络、丰富李雅普诺夫函数参数化、构建直接优化吸引域的半定规划四方面改进基于半代数集的验证方法，数值算例验证了其价值。
2025-10-28 cs.SY eess.SY
(B)LOCKBOX -- Secure Software Architecture with Blockchain Verification
据专家称，今天所有IT漏洞中有三分之一是由于软件验证不足。内部程序进程没有足够的安全来防止攻击者的操纵，特别是如果已经获得访问权限。缺乏能够监测和控制程序流程的内部控制实例。特别是当软件漏洞变得已知时，需要迅速采取行动，由此对单个应用程序的后果通常是不可预见的。通过我们的方法（B）LOCKBOX，软件构建块充当基于交易的区块链网络中的验证实体。源代码、二进制文件和应用程序的执行受到监督。分布式系统的完整性防止了不必要的干扰和操纵。
2022-11-21 cs.CR cs.DC cs.SY
Certified Set Convergence for Piecewise Affine Systems
Technical University of Munich（慕尼黑工业大学）；Hainan Bielefeld University of Applied Sciences（海南比勒费尔德应用科学大学）
本文提出通过神经Lyapunov函数认证分段仿射系统在有界扰动下的集收敛，采用Hamilton-Jacobi反向可达性训练的价值函数和排列不变的Deep Sets控制器，实现对整个状态集的验证，保证在不同模式下集的收敛。
2026-11-10 cs.SY eess.SY
LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction
University of Waterloo（滑铁卢大学）；University of Illinois（伊利诺伊大学）
本文介绍LyZNet，一个基于PINN和SMT求解器学习并验证神经Lyapunov函数及接近吸引域的轻量级Python工具，适用于非线性系统稳定性分析。
2024-03-15 cs.LG cs.SY eess.SY
Proofs for an Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions
Aalborg University（奥尔堡大学）
本文提出并证明了一种基于Lyapunov函数子水平集划分状态空间、通过时间自动机抽象连续动力系统的方法，并证明了对于Morse-Smale系统存在可靠抽象，对于线性系统存在完备且可精化的抽象。
2010-08-19 cs.SY eess.SY
Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation
MIT（麻省理工学院）；Toyota Research Institute（丰田研究所）；UCLA（加利福尼亚大学洛杉矶分校）；UIUC（伊利诺伊大学厄巴纳-香槟分校）
本文提出一种新框架，通过经验证伪与策略性正则化联合学习神经网络控制器和李雅普诺夫证书，扩大可验证吸引域，并首次实现具有形式化稳定性保证的神经网络输出反馈控制。
2024-06-05 cs.AI cs.LG cs.RO
Dynamic System Stability Verification Using Numerical Simulator
针对安全关键系统中基于仿真的控制设计缺乏稳定性和鲁棒性保证的问题，提出基于扩展逆 Lyapunov 定理的计算方法，通过数值模拟器验证动态系统指数稳定性，并利用有限采样算法提供确定性稳定性保证。
2023-11-19 cs.SY eess.SY math.DS
Improved Sum-of-Squares Stability Verification of Neural-Network-Based Controllers
本文改进了基于半代数集和凸半定规划的神经网络控制系统闭环稳定性验证框架，通过引入新激活函数兼容RENs和RNNs，提出替代证明及两个简化局部稳定性和吸引域分析的新优化问题，并在数值示例中验证了有效性。
2025-07-14 cs.SY eess.SY
Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program
许多粒子加速器的一个重要方面是不断发展和频繁的配置变化，需要执行它们设计的实验。这通常会导致可配置软件的设计，可以吸收这些变化，并执行所需的控制和保护行动。这种设计策略最大限度地降低了工程和维护成本，但它使软件验证活动更具挑战性，因为必须保证任何可能的配置的安全属性。软件模型检验是一种广泛应用的自动化验证技术。这种验证方法探索系统模型的所有可能组合，以保证其符合某些属性或规范。这对于高度可配置的软件来说是一种非常合适的技术，因为通常有大量的组合需要检查。本文介绍了如何PLCverif，欧洲核子研究中心的模型检验平台，已被应用到一个高度可配置的可编程逻辑控制器（PLC）程序，SPS人员保护系统（PPS）。这种验证方法的好处和挑战也进行了讨论。
2022-03-30 cs.SE cs.SY eess.SY
Lyapunov-stable neural-network control
Toyota Research Institute（丰田研究院）；Stanford University（斯坦福大学）；Massachusetts Institute of Technology（麻省理工学院）
深度学习对机器人技术产生了深远的影响。具体来说，深度强化学习算法在为各种任务合成神经网络控制器方面非常有效。然而，尽管这种经验上的成功，这些控制器仍然缺乏对它们的性能的理论保证，例如李雅普诺夫稳定性（即，保证闭环系统的所有轨迹在控制策略下收敛到目标状态）。这与传统的基于模型的控制器设计形成鲜明对比，其中原则方法（如LQR）可以合成具有可证明保证的稳定控制器。为了解决这一差距，我们提出了一种通用的方法来合成一个李雅普诺夫稳定的神经网络控制器，连同一个神经网络李雅普诺夫函数，同时证明其稳定性。我们的方法制定了一个混合整数线性规划（MIP）的李雅普诺夫条件验证。我们的MIP验证器要么证明李雅普诺夫条件，或生成反例，可以帮助改善候选控制器和李雅普诺夫函数。我们还提出了一个优化程序来计算内近似的闭环系统的吸引区域。我们应用我们的方法，包括倒立摆，2D和3D四旋翼机器人，并展示我们的神经网络控制器优于基线LQR控制器。代码在\url{https://github.com/StanfordASL/neural-network-lyapunov}上开源。
2021-09-29 cs.RO cs.SY eess.SY
Verifying Switched System Stability With Logic
切换系统表现出微妙的（不）稳定行为，要求系统设计者仔细分析闭环系统的稳定性，从他们提出的切换控制律。本文提出了一种形式化的方法来验证切换系统的稳定性，融合了经典的思想，从控制和验证文献使用微分动态逻辑（dL），逻辑演绎验证的混杂系统。从控制，我们使用标准的稳定性概念，各类开关机制和相应的李雅普诺夫函数为基础的分析技术。从验证，我们使用dL的能力，以验证量化属性的混杂系统和切换系统的dL模型作为循环的混合程序，其稳定性可以正式指定和证明，通过找到适当的循环不变量，即，在每次循环迭代中保留的属性。这种思想的融合使基于dL的KeYmaera X证明器能够可靠地实现切换系统稳定性验证。对于标准类的开关机制，实现提供了全自动的稳定性证明，包括搜索合适的李雅普诺夫函数。此外，演绎方法的一般性还使得能够通过适当地表达这些控制律背后的特定直觉的回路不变量的设计来验证需要非标准稳定性参数的切换控制律。这种灵活性证明了三个案例研究：一个模型的纵向飞行控制的Branicky，自动巡航控制器，和Brockett的非完整积分。
2022-04-08 cs.LO cs.SY eess.SY
Testing and verification of neural-network-based safety-critical control software: A systematic literature review
Norwegian University of Science and Technology（挪威科技大学）；Southwest Jiaotong University（西南交通大学）
背景：神经网络（NN）算法已经成功地应用于许多安全关键的网络物理系统（SCCPS）。基于神经网络的控制软件的测试与验证（T&V）是软件工程和安全工程研究者和实践者关注的热点。目的：随着对基于神经网络的控制软件在安全关键领域的T&V研究的增加，重要的是系统地回顾最先进的T&V方法，对发明的方法和工具进行分类，并确定未来研究的挑战和差距。方法：检索950篇关于神经网络安全关键控制软件（SCCS）测试与验证的文献。为了达到我们的结果，我们过滤了2001年至2018年期间发表的83篇主要论文，应用主题分析方法分析了从选定论文中提取的数据，介绍了方法的分类，并确定了挑战。结论：这些方法分为五个高阶主题：确保神经网络的鲁棒性，确保基于神经网络的控制软件的安全性，提高神经网络的故障恢复能力，测量和确保测试的完整性，提高神经网络的可解释性。从行业的角度来看，提高NN的可解释性是安全关键型应用的关键需求。我们还调查了四个主要安全生命周期阶段中的九个安全完整性属性，以调查IEC 61508-3中T&V目标的实现水平。结果表明，正确性、完整性、无内在错误和容错是研究界最关注的问题。然而，很少的努力已经投入到实现可重复性，没有审查的研究集中在精确定义的测试配置或对常见原因故障的防御。
2020-03-20 cs.LG cs.SE cs.SY
