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

TL;DR

This paper develops barrier-like conditions that are both necessary and sufficient for infinite-horizon safety and reach-avoid verification of stochastic discrete-time systems, advancing beyond prior methods that only provided sufficient conditions.

Contribution

It introduces a rigorous framework of barrier-like conditions that precisely characterize safety and reach-avoid properties, establishing both necessity and sufficiency for stochastic systems.

Findings

Established necessary and sufficient barrier conditions for safety verification.

Derived conditions for reach-avoid properties involving probabilistic guarantees.

Provided a relaxation of Bellman equations to facilitate verification.

Abstract

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.