Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems

This paper investigates necessary and sufficient barrier-like conditions for infinite-horizon safety and reach-avoid verification of stochastic discrete-time systems, derived via a relaxation of the Bellman equations. Unlike prior approaches that primarily focus on sufficient conditions, our work rigorously establishes both necessity and sufficiency for infinite-horizon properties. Safety verification concerns certifying that, starting from a given initial state, the system remains within a safe set at all future time steps with probability at least equal to a specified threshold. For this purpose, we formulate a necessary and sufficient barrier-like condition that captures this infinite-time safety property. In contrast, reach-avoid verification generalizes safety verification by also incorporating reachability. Specifically, it aims to ensure that the probability of the system, starting from a given initial state, eventually reaching a target set while remaining within the safe set until the first hit of the target is no less than a prescribed bound. Under suitable assumptions, we establish two necessary and sufficient barrier-like conditions for this reach-avoid specification.