Stochastic Lyapunov-Barrier Functions for Robust Probabilistic Reach-Avoid-Stay Specifications

• 成果类型: Article
• 署名作者: Meng, Yiming; Liu, Jun
• 署名单位: University of Waterloo
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2024.3368867
• 发表日期: 2024
• 页码: 5470-5477
• 关键词: Probabilistic logic; safety; TOPOLOGY; Stochastic processes; Stability criteria; Numerical stability; dynamical systems; Control synthesis; probabilistic reach-avoid-stay specifications; probabilistic stability and safety with robustness; stochastic Lyapunov-barrier functions; stochastic dynamical systems; weak topology

摘要

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 probabilistic reach-avoid-stay problems in consideration of robustness. To this end, based on the weak topology, we first establish a connection between probabilistic 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 Lyapunov-barrier conditions in control synthesis for reach-avoid-stay specifications, and show its effectiveness in a case study.