论文标题
Lyapunov驻式荷兰式避免距离静止式静止 - 杂种系统的表征
Lyapunov-Barrier Characterization of Robust Reach-Avoid-Stay Specifications for Hybrid Systems
论文作者
论文摘要
稳定性，可及性和安全性是动态系统的关键特性。虽然可以通过基于抽象的形式方法有效地处理验证和控制综合目标，但由于使用状态空间离散化，这种方法在计算上可能很昂贵。相比之下，Lyapunov的方法定性地表征了稳定性和安全性能，而没有任何状态空间离散化。关于匡威Lyapunov - 鲍尔定理的最新工作也表明了由非线性微分方程建模的系统的近似完整性或验证避免距离停机的规格。在本文中，基于杂种弧的拓扑结构，我们将Lyapunov绑架的表征扩展到了由差分和差异夹杂物描述的更通用的混合系统。我们表明，Lyapunov绑架功能不仅足以保证适当的混合动力系统的Aver-Avoid-Stay规格，而且对于在轻度条件下任意稍微扰动的系统也是必要的。提供数值示例以说明主要结果。
Stability, reachability, and safety are crucial properties of dynamical systems. While verification and control synthesis of reach-avoid-stay objectives can be effectively handled by abstraction-based formal methods, such approaches can be computationally expensive due to the use of state-space discretization. In contrast, Lyapunov methods qualitatively characterize stability and safety properties without any state-space discretization. Recent work on converse Lyapunov-barrier theorems also demonstrates an approximate completeness or verifying reach-avoid-stay specifications of systems modelled by nonlinear differential equations. In this paper, based on the topology of hybrid arcs, we extend the Lyapunov-barrier characterization to more general hybrid systems described by differential and difference inclusions. We show that Lyapunov-barrier functions are not only sufficient to guarantee reach-avoid-stay specifications for well-posed hybrid systems, but also necessary for arbitrarily slightly perturbed systems under mild conditions. Numerical examples are provided to illustrate the main results.
