Reach-avoid Verification using Lyapunov Densities
可达性分析将施工安全和具体进度保证结合起来，能够将许多重要的工程问题形式化。本文利用李雅普诺夫密度研究了由常微分方程建模的系统的可达性验证问题。首先，考虑弱到达-避免验证。给定初始集合、安全集合和目标集合，弱到达-避免验证是验证到达-避免属性（即，系统将最终进入目标集合，同时在第一目标命中时间之前停留在安全集合内）对于初始集合中的几乎所有状态都成立。我们提出了两个新的充分条件，利用李雅普诺夫密度的弱到达-避免验证。这两个充分条件被证明是比现有的更弱，提供了更多的可能性验证弱到达-避免性质成功。然后，我们将这些条件推广到初始集合中所有状态的到达-避免性质的验证。最后，一个例子表明所提出的条件的理论发展。
2023-02-06 cs.SY eess.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
Automated Stability Analysis of Piecewise Affine Dynamics Using Vertices
本文针对 PWA 动力系统，提出基于候选 Lyapunov 函数导数符号或向量场变化、并结合 Delaunay 三角剖分的自动多面体划分方法，以更少区域和更短计算时间找到稳定性证书。
2023-12-05 cs.SY eess.SY
Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers
Vanderbilt University（范德堡大学）
本文针对具有神经网络控制器的分段线性系统，提出分层方法计算ReLU神经网络的输出可达集，并通过迭代估计反馈控制系统的可达集以实现安全验证。
2018-02-20 cs.SY eess.SY
A piecewise ellipsoidal reachable set estimation method for continuous bimodal piecewise affine systems
Quy Nhon University（归仁大学）；Delft University of Technology（代尔夫特理工大学）
本文提出一种基于分段二次李雅普诺夫函数的可达集估计方法，用于简化双模分段仿射系统的可达性分析。
2021-06-12 cs.SY eess.SY
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
Dwell-Time Based Stability Analysis and L2 Control of LPV Systems with Piecewise Constant Parameters and Delay
利用钟依赖Lyapunov-Krasovskii泛函，得到了一类具有时变时滞的分段常参数LPV系统基于驻留时间的稳定性条件.还提供了保证L2性能的时钟依赖增益调度状态反馈控制器的充分综合条件。几个数值和实际的例子，以说明的结果的有效性，给出。
2020-03-10 cs.SY eess.SY
Model Reference Adaptive Control of Piecewise Affine Systems with State Tracking Performance Guarantees
本文研究不确定分段仿射系统的模型参考自适应控制方法。所提出的方法确保误差度量，定义为加权欧几里德范数的状态跟踪误差，被限制在用户定义的时变性能范围内。我们引入一个辅助性能函数来构造一个障碍李雅普诺夫函数。该辅助性能信号在每个切换时刻被复位，这防止了由切换时刻的误差度量的跳变引起的障碍的越过。基于用户定义的性能界限和辅助性能函数的参数导出停留时间约束。我们还证明了李雅普诺夫函数是非增加的，即使在切换瞬间，因此不施加额外的停留时间的限制。此外，我们提出了鲁棒修改的自适应控制器的不确定分段仿射系统的非匹配干扰。数值算例验证了该方法的正确性。
2021-03-04 cs.SY eess.SY
Optimization of Lyapunov Invariants in Verification of Software Systems
Massachusetts Institute of Technology（麻省理工学院）；Georgia Institute of Technology（佐治亚理工学院）
提出一种基于控制理论的框架，通过将李雅普诺夫函数和凸优化技术应用于数值软件系统验证，解决安全性和性能规范（如无溢出、无除零、有限时间终止等）的验证问题，核心是构造并优化李雅普诺夫不变量。
2011-07-31 cs.SY eess.SY math.OC
Formal Verification of Control Lyapunov-Barrier Functions for Safe Stabilization with Bounded Controls
针对有界控制下的安全镇定问题，提出可验证条件合成单光滑李雅普诺夫函数以同时保证渐近稳定性和安全性，构造显式CLBF且比基于SOS的兼容CBF-CLF设计保守性更低。
2025-11-13 cs.SY eess.SY math.OC
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
Counterexample-guided computation of polyhedral Lyapunov functions for hybrid systems
针对不确定连续时间线性混杂系统，提出了一种计算凸分段线性（多面体）李雅普诺夫函数的反例引导迭代算法。多面体李雅普诺夫函数提供了一种替代常用的多项式李雅普诺夫函数。我们的方法首先表征多面体李雅普诺夫函数的内在属性，包括其“偏心率”和“鲁棒性”的扰动。然后，我们推导出一个算法，要么计算一个多面体李雅普诺夫函数证明系统是稳定的，或得出结论，没有多面体李雅普诺夫函数存在的偏心率和鲁棒性参数满足一些用户提供的限制。值得注意的是，我们的方法没有先验界限的线性件，使所需的多面体李雅普诺夫函数的数量。该算法在学习步骤和验证步骤之间交替，始终保持证人状态的有限集。学习步骤求解线性规划以计算与见证状态的有限集兼容的候选李雅普诺夫函数。在验证步骤中，我们的方法验证候选的李雅普诺夫函数是否是一个有效的李雅普诺夫函数的系统。如果验证失败，我们会获得一个新的证人。我们证明了我们的算法所需的最大迭代次数的理论界。我们证明了该算法的数值例子的适用性。
2022-06-22 cs.SY eess.SY math.OC
Stability Analysis and State-Feedback Stabilization of LPV Time-Delay Systems with Piecewise Constant Parameters subject to Spontaneous Poissonian Jumps
本文讨论了具有参数依赖时滞的线性变参数系统在参数为随机分段常数的条件下的Poissonian跳跃的稳定性分析。基于随机Lyapunov-Krasovskii泛函，我们还提供了充分的综合条件的增益调度状态反馈控制器的记忆参数依赖的线性矩阵不等式（LMI）。由于积分项的存在，这种合成条件在计算上是难以处理的。然而，我们表明，这些LMI可以等价地表示为积分自由的LMI，这是计算上容易处理的。最后通过实例说明了所得结果的适用性。
2021-02-09 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
Estimation of Constraint Admissible Invariant Set with Neural Lyapunov Function
本文提出利用分段仿射神经李雅普诺夫函数，将最大约束容许正不变集估计问题转化为多个线性规划，并训练学习型估计器从参考实时推断CAPI集，用于一般参考跟踪控制与显式参考调节器。
2024-09-30 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
Stochastic Stability Analysis of Discrete Time System Using Lyapunov Measure
Iowa State University（爱荷华州立大学）
本文研究了随机非线性离散时间系统的稳定性问题，提出基于线性转移算子的李雅普诺夫度量作为稳定性验证工具，并建立了李雅普诺夫函数与度量之间的联系，通过双算子性质展示其对偶性，提出有限维近似方法和粗随机稳定性概念。
2016-03-08 cs.SY eess.SY math.DS
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
Incremental stability of Lur'e systems through piecewise-affine approximations
本文提出用于评估Lur'e系统增量渐近稳定的条件，比增量圆准则更非保守。通过将非线性近似为分段仿射函数，提供线性矩阵不等式条件以构造连续分段二次Lyapunov函数。
2016-11-25 cs.SY eess.SY
Adaptive Meshing for CPA Lyapunov Function Synthesis
Thomas Lord Department of Mechanical Engineering and Materials Science, Duke University（杜克大学托马斯·劳德机械与材料工程系）；Department of Aeronautics and Astronautics, Stanford University（斯坦福大学航空与航天工程系）
本文提出三种方法用于更高效地生成李雅普诺夫函数网格，以降低计算成本。
2026-09-09 cs.SY eess.SY
Systematic, Lyapunov-Based, Safe and Stabilizing Controller Synthesis for Constrained Nonlinear Systems
针对状态和输入受限的非线性系统，提出了一种同时寻找连续分段仿射（CPA）类Lyapunov函数和控制器的控制器综合方法.非凸优化问题的可接受的状态，可以细化，以满足主要的控制目标，如稳定性和安全性，以及次要的性能目标的三角形子集制定。一个多阶段的设计也给出了扩大区域的吸引力（ROA）顺序，同时允许每个阶段的独家性能。由所得的Lipschitz李雅普诺夫函数得到了闭环系统ROA不变子集的清晰边界。对于控制仿射非线性系统，非凸问题被表述为一系列保守的、适定的半定规划。这些迭代地降低代价函数，直到满足设计目标。由于所得的CPA类李雅普诺夫函数也是Lipschitz控制（或障碍）李雅普诺夫函数，它们可以用于在线二次规划，以找到最小范数控制输入。数值算例验证了该方法的有效性。
2022-03-05 cs.SY eess.SY
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
Guaranteed Time Control using Linear Matrix Inequalities
Universidade Federal de Minas Gerais（米纳斯吉拉斯联邦大学）；Instituto Federal de Minas Gerais（米纳斯吉拉斯联邦理工学院）；University of São Paulo（圣保罗大学）；Université Polytechnique Hauts-de-France（上法兰西理工大学）
本文提出一种方法，通过谐波变换Lyapunov函数和分段二次表示，保证在考虑不确定性和输入状态约束时，达到非零测度目标集的最短时间上界。
2026-04-17 cs.SY eess.SY
Graph-Based Conditions for Feedback Stabilization of Switched and LPV Systems
本文提出基于图论和路径完备李雅普诺夫函数的新条件，通过LMI设计切换线性系统的鲁棒和模式依赖分段线性反馈控制器，实现镇定。
2023-06-20 cs.SY eess.SY math.OC
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
Simultaneous Controller and Lyapunov Function Design for Constrained Nonlinear Systems
本文提出了一种利用容许状态集的可变三角剖分的离线优化来镇定状态和输入受限的非线性系统的方法。对于控制仿射系统，通过选择连续的分段仿射（CPA）控制器结构，将非凸优化问题转化为迭代半定规划（SDP）问题，利用现有的软件可以有效地求解。该方法对系统的动力学和约束条件有非常一般的假设。与类似的现有方法不同，它避免了寻找终端不变集，解决非凸优化，并且不依赖于知道控制李雅普诺夫函数（CLF），因为它明确地找到了CPA李雅普诺夫函数。该方法对状态范数的衰减率强制执行所需的上限，并找到确切的吸引区域。因此，它也可以被看作是一个系统的方法，寻找Lipschitz CLF的状态和输入约束控制仿射系统。使用CLF，最小范数控制器也制定了二次规划在线应用。
2021-12-01 cs.SY eess.SY
Finite-time stability properties of Lur'e systems with piecewise continuous nonlinearities
利用Lur 'e-Postnikov李雅普诺夫函数的集值李导数的概念，分析了具有分段连续非线性项的Lur' e系统的稳定性.我们首先推广了文献中的一个结果，在更一般的扇形条件下建立了原点的全局渐近稳定性。然后，我们提出了这项工作的主要成果，即额外的条件下，输出和状态的有限时间稳定性也认为是一类系统。我们强调这些结果的相关性，通过证明两个已知的工程系统的稳定性：受摩擦和细胞神经网络影响的机械系统。
2023-02-02 cs.SY eess.SY math.DS
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
Lower Bounds on Complexity of Lyapunov Functions for Switched Linear Systems
Princeton University（普林斯顿大学）；ICTEAM Institute, Université catholique de Louvain（天主教鲁汶大学 ICTEAM 研究所）
研究显示，对于任意正整数d，存在固定维数的切换线性系统，其在任意切换下稳定但不具有多项式、多面体或分段二次Lyapunov函数。该结论表明无法为寻找此类稳定性证书的线性或半正定规划设定上界。
2015-04-15 cs.CC 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
Continuity Conditions for Piecewise Quadratic Functions on Simplicial Conic Partitions are Equivalent
Eindhoven University of Technology（埃因霍温理工大学）
本文证明了在单纯形锥划分上，分式二次函数的连续性条件是等价的，从而简化了分析中的选择依据。
2025-11-06 cs.SY eess.SY math.OC
Proofs for an Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions
Aalborg University（奥尔堡大学）
本文提出并证明了一种基于Lyapunov函数子水平集划分状态空间、通过时间自动机抽象连续动力系统的方法，并证明了对于Morse-Smale系统存在可靠抽象，对于线性系统存在完备且可精化的抽象。
2010-08-19 cs.SY eess.SY
Deep Reinforcement Learning Graphs: Feedback Motion Planning via Neural Lyapunov Verification
本文提出一种基于深度强化学习控制器图与神经网络的反馈运动规划算法，通过树结构和图结构两种连接方式分别实现点到点和空间到空间控制，并在一阶动态系统上验证了其有效性。
2023-11-29 cs.RO cs.SY eess.SY
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
Control Lyapunov Function Design via Configuration-Constrained Polyhedral Computing
该研究利用构型约束多面体计算技术设计约束线性系统的分段仿射凸控制李雅普诺夫函数，推广至含加性和乘性扰动的不确定系统，仅需单阶段凸优化即可逼近两类最优控制问题的无限时域代价函数，可应用于显式控制及MPC终端设计。
2025-03-20 cs.SY eess.SY math.OC
Learning Region of Attraction for Nonlinear Systems
估计一般非线性自治系统的吸引域（ROA）仍然是一个具有挑战性的问题，需要逐案分析。利用神经网络的普适逼近特性，提出了一种反例引导的方法来估计一般非线性动力系统的ROA，前提是它们可以用分段线性神经网络逼近，且逼近误差有界.具体来说，我们的方法使用反例搜索鲁棒的李雅普诺夫函数，即，李雅普诺夫条件失效的状态。我们使用混合二次规划生成反例。我们的方法是保证找到一个强大的李雅普诺夫函数在参数化的函数类，如果存在的话，在收集有限数量的反例。我们通过数值例子来说明我们的方法。
2021-10-02 cs.SY eess.SY
Improved Sum-of-Squares Stability Verification of Neural-Network-Based Controllers
本文改进了基于半代数集和凸半定规划的神经网络控制系统闭环稳定性验证框架，通过引入新激活函数兼容RENs和RNNs，提出替代证明及两个简化局部稳定性和吸引域分析的新优化问题，并在数值示例中验证了有效性。
2025-07-14 cs.SY eess.SY
OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems
Stanford University（斯坦福大学）
深度学习方法可用于生成控制策略，但证明其安全性具有挑战性。由此产生的网络是非线性的，并且通常非常大。为了应对这一挑战，我们提出了OVERT：一个健全的算法的安全性验证的非线性离散时间闭环动态系统的神经网络控制策略。OVERT的新颖之处在于将经典形式化方法文献中的思想与较新的神经网络验证文献中的思想相结合。OVERT的核心概念是抽象非线性函数，并给出一组最优紧的分段线性边界。这种分段线性边界被设计用于无缝集成到ReLU神经网络验证工具中。OVERT可以通过计算可达集或直接求解可行性查询来证明有界时间安全性。我们展示了几个经典基准测试示例的安全验证的各种示例。OVERT在计算时间和可达集的紧密性方面都优于现有的方法。
2021-08-03 cs.LG cs.LO cs.SY
Control of Uncertain PWA Systems using Difference-of-Convex Decompositions
在这份报告中，我们分析和设计反馈策略的离散时间分段仿射（PWA）系统的仿射动力学和多面体分区的不确定性。其主要思想是利用连续PWA系统的差分凸（DC）分解，以获得二次李雅普诺夫函数作为稳定性证书和稳定的仿射策略在一个更高的维度空间。当投影回状态空间时，我们得到时变PWQ李雅普诺夫函数和时变PWA反馈策略。
2023-03-20 cs.SY eess.SY math.OC
Lyapunov Neural Network with Region of Attraction Search
提出一种Lyapunov神经网络，通过构造确保非负性和唯一全局最小值，并最大化水平集内切正方形以扩大吸引域，加速控制器与Lyapunov证书的求解，在多个系统上训练时间减半且ROA更大。
2024-03-15 cs.SY eess.SY
SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions
Washington University in St. Louis（圣路易斯华盛顿大学）；University of California, San Diego（加利福尼亚大学圣迭戈分校）
针对 ReLU NCBF 精确安全验证中激活区域枚举成本高的问题，提出 SEEV 框架，通过边界正则化与紧致过近似验证提升效率并保持 CBF 质量。
2024-10-27 cs.RO cs.SY eess.SY
SEROAISE: Advancing ROA Estimation for ReLU and PWA Dynamics through Estimating Certified Invariant Sets
本文提出SEROAISE框架，通过在认证PWA不变集上计算类Lyapunov PWA函数，为ReLU神经网络和PWA动态系统构建吸引域，利用IISE和NUGIS提升估计性能，优于传统方法。
2025-04-16 cs.SY eess.SY
Data-Driven Reachability Analysis for Piecewise Affine Systems
Technical University of Munich（慕尼黑工业大学）；University of Trieste（的里雅斯特大学）
本文提出了一种基于混合锥体的数据驱动可达性分析方法，用于解决分段仿射系统中动态突变区域边界的问题，并评估了考虑测量噪声的集合估计方法。
2026-02-17 cs.SY eess.SY
Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs
Onera, the French Aerospace Lab（法国航空航天实验室）；Université de Toulouse（图卢兹大学）
本文提出通过分段仿射程序分析，利用分段二次李雅普诺夫函数计算可达集的上界，以处理动态系统控制器的静态分析问题。
2014-09-16 cs.SY eess.SY math.OC
Learning Control Lyapunov Functions from Counterexamples and Demonstrations
University of Colorado, Boulder（科罗拉多大学博尔德分校）
本文提出了一种学习控制李雅普诺夫函数的技术，通过迭代过程结合反例和演示来生成控制器，用于非线性动态系统的稳定性和安全性保证。
2019-06-05 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
The First Open-Source Framework for Learning Stability Certificates from Data
Stable Robotics Limited（Stable Robotics有限公司）
本文提出首个开源框架，通过数据驱动方法从真实民航数据中学习Lyapunov函数，用于评估系统稳定性。
2025-11-22 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
Learning Piecewise Residuals of Control Barrier Functions for Safety of Switching Systems using Multi-Output Gaussian Processes
University of Waterloo（滑铁卢大学）
本文提出一种基于多输出高斯过程的学习控制策略，通过近似切换系统中控制障碍函数和控制李雅普诺夫函数的分段残差，将机会约束转化为凸优化，确保系统在模型不确定性下的安全性。
2024-04-18 cs.RO cs.SY eess.SY
Joint Differentiable Optimization and Verification for Certified Reinforcement Learning
Northwestern University（西北大学）；UC Berkeley（加州大学伯克利分校）；University of Liverpool（利物浦大学）；Yale University（耶鲁大学）
在用于安全关键控制系统的基于模型的强化学习中，重要的是正式证明系统属性（例如，安全性、稳定性）。然而，由于现有的方法通常应用形式化验证\emph{after}，控制器已经被学习，有时很难获得任何证书，即使在学习和验证之间的多次迭代之后。为了应对这一挑战，我们提出了一个框架，通过制定和解决一个新的双层优化问题，这是可区分的梯度从价值函数和证书，联合进行强化学习和形式化验证。各种例子上的实验表明，我们的框架显着的优势，基于模型的随机值梯度（SVG）的方法和无模型的近端策略优化（PPO）的方法在寻找可行的控制器，障碍功能和李雅普诺夫函数，确保系统的安全性和稳定性。
2023-03-21 cs.LG cs.SY eess.SY
