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

TL;DR

This paper develops sufficient conditions using stochastic Lyapunov-barrier functions to ensure robustness in probabilistic reach-avoid-stay specifications for stochastic dynamical systems, enhancing safety and stability guarantees.

Contribution

It introduces a stochastic version of Lyapunov-barrier functions providing sufficient conditions for probabilistic reach-avoid-stay objectives in stochastic systems.

Findings

Established a connection between stochastic stability and reach-avoid-stay specifications.

Proved that stochastic Lyapunov-barrier functions offer sufficient conditions for safety objectives.

Demonstrated the effectiveness of the approach in a case study.

Abstract

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.