论文标题
使用随机Lyapunov携带函数的足够稳健概率到达避免停机的规格的足够条件
Sufficient Conditions for Robust Probabilistic Reach-Avoid-Stay Specifications using Stochastic Lyapunov-Barrier Functions
论文作者
论文摘要
稳定性和安全性对于动态系统的安全关键控制至关重要。可以通过正式方法以及具有健全性和近似完整性保证的Lyapunov方法有效地处理确定性动力学系统的Aver-Avoid-Stay目标。但是，对于连续的时间随机动力学系统，概率避免到达的问题被视为具有挑战性的任务。由于使用Lyapunov驱动器功能来表征安全至关重要性能的近期应用激励，我们旨在为稳健性提供随机版本的概率Aver-Avaid-Stay问题。为此，我们首先在随机稳定性与安全限制与远距离安装规格之间建立了联系。然后，我们证明了随机Lyapunov绑架功能为目标提供了足够的条件。我们将lyapunovbarrier条件应用于控制合成中，以实现Aver-Avoid-Stay规格，并在案例研究中显示其有效性。
Stability and safety are crucial in safety-critical control of dynamical systems. The reach-avoid-stay objectives for deterministic dynamical systems can be effectively handled by formal methods as well as Lyapunov methods with soundness and approximate completeness guarantees. However, for continuous-time stochastic dynamical systems, probabilistic reach-avoid-stay problems are viewed as challenging tasks. Motivated by the recent surge of applications in characterizing safety-critical properties using Lyapunov-barrier functions, we aim to provide a stochastic version for the probabilistic reach-avoid-stay problems in consideration of robustness. To this end, we first establish a connection between stochastic stability with safety constraints and reach-avoid-stay specifications. We then prove that stochastic Lyapunov-barrier functions provide sufficient conditions for the target objectives. We apply Lyapunovbarrier conditions in control synthesis for reach-avoid-stay specifications, and show its effectiveness in a case study.
