2022/03/23 by Yiming Meng, Jun Liu, Meng, Yiming +1 · 2 citations
Computer Science · Engineering · #Dynamical Systems (math.DS) #FOS: Mathematics #Formal Methods in Verification #Petri Nets in System Modeling #Systems Engineering Methodologies and Applications
paper · pdf · doi:10.48550/arxiv.2203.12746
openalex publication_date 2022/03/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.