Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
Bai Xue
TL;DR
This work establishes necessary and sufficient barrier-like conditions for proving infinite-horizon safety and reach-avoid properties in stochastic discrete-time systems by relaxing Bellman equations to yield verifiable barrier functions. It first derives a barrier condition for safety using a value function that characterizes the exact safety probability, and then extends the framework to reach-avoid verification, presenting two cases: RA I under finite-time almost-sure exit/reach, and RA II under a discounted, strictly-bounded scenario without a key assumption. The contributions provide a principled, mathematically rigorous route to certify lower bounds on safety and RA probabilities via barrier-like inequalities, with implications for convex optimization and controller synthesis in stochastic settings. The paper also discusses limitations and future directions, including finite-horizon analyses and efficient numerical methods to handle the barrier constraints in practice.
Abstract
In this paper, we examine necessary and sufficient barrier-like conditions for infinite-horizon safety verification and reach-avoid verification of stochastic discrete-time systems, derived through a relaxation of Bellman equations. Unlike previous methods focused on barrier-like conditions that primarily address sufficiency, our work rigorously integrates both necessity and sufficiency for properties pertaining to infinite time. Safety verification aims to certify the satisfaction of the safety property, which stipulates that the probability of the system, starting from a specified initial state, remaining within a safe set always is greater than or equal to a specified lower bound. A necessary and sufficient barrier-like condition is formulated for safety verification. In contrast, reach-avoid verification extends beyond safety to include reachability, seeking to certify the satisfaction of the reach-avoid property. It requires that the probability of the system, starting from a specified initial state, reaching a target set eventually while remaining within a safe set until the first hit of the target, is greater than or equal to a specified lower bound. Two necessary and sufficient barrier-like conditions are formulated under certain assumptions.