Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
Bai Xue
TL;DR
The paper addresses finite-time safety and reach-avoid verification for stochastic discrete-time systems over a finite horizon $[0,N]$ by introducing barrier-like sufficient conditions that yield explicit lower and upper bounds on exit, reach, and reach-avoid probabilities. The core idea is to construct barrier functions $v(\bm{x})$ on augmented domains (e.g., $\widetilde{\mathcal{X}}$ and $\widehat{\mathcal{X}}$) and enforce $\mathbb{E}[v(\bm{\phi}(1))] \le \frac{v(\bm{x})}{\alpha}+\beta$ (or its variants) to obtain computable finite-time bounds with parameters $\alpha$ and $\beta$. The methodology extends existing infinite-horizon barrier techniques by enabling finite-horizon guarantees without requiring the strong invariant-set assumption and by providing both lower and upper bounds for safety and reach-avoid problems. Two 1D numerical examples illustrate the approach, solved via semidefinite programming/SOS to synthesize polynomial barrier certificates, with tighter bounds achieved at higher polynomial degrees, and a discussion of the practical limitations and directions for future work on algorithmic improvements and necessity analyses.
Abstract
This paper studies finite-time safety and reach-avoid verification for stochastic discrete-time dynamical systems. The aim is to ascertain lower and upper bounds of the probability that, within a predefined finite-time horizon, a system starting from an initial state in a safe set will either exit the safe set (safety verification) or reach a target set while remaining within the safe set until the first encounter with the target (reach-avoid verification). We introduce novel barrier-like sufficient conditions for characterizing these bounds, which either complement existing ones or fill gaps. Finally, we demonstrate the efficacy of these conditions on two examples.