A Unifying Perspective for Safety of Stochastic Systems: From Barrier Functions to Finite Abstractions

TL;DR

This work unifies safety verification for discrete-time stochastic systems by viewing stochastic barrier functions and finite abstractions as approximations of a single stochastic dynamic programming problem. It proves that the optimal safety probability can be achieved by deterministic Markov policies and shows how SBFs and interval-based abstractions yield computable, provable lower bounds within this DP framework. Abstractions to IMDPs provide asymptotically optimal safety certificates as partitions become finer, at the cost of increased computation, while SBFs offer potentially faster but conservative guarantees with no general convergence to the true optimum. The results enable a principled comparison and guide the choice of method based on desired guarantees and computational resources, with proofs of optimality and convergence for the abstraction-based approach and formal bounds for barrier-based methods.

Abstract

Providing safety guarantees for stochastic dynamical systems is a central problem in various fields, including control theory, machine learning, and robotics. Existing methods either employ Stochastic Barrier Functions (SBFs) or rely on numerical approaches based on finite abstractions. SBFs, analogous to Lyapunov functions, are used to establish (probabilistic) set invariance, whereas abstraction-based approaches approximate the stochastic system with a finite model to compute safety probability bounds. This paper presents a unifying perspective on these seemingly different approaches. Specifically, we show that both methods can be interpreted as approximations of a stochastic dynamic programming problem. This perspective allows us to formally establish the correctness of both techniques, characterize their convergence and optimality properties, and analyze their respective assumptions, advantages, and limitations. Our analysis reveals that, unlike SBFs-based methods, abstraction-based approaches can provide asymptotically optimal safety certificates, albeit at the cost of increased computational effort.

Figures (2)

• Figure 1: For a stochastic system $\mathbf{x}[k+1]=\mathbf{x}[k] + \mathbf{v}$, where $\mathbf{v}\sim \mathcal{N}(0,0.1)$ is an independent additive zero-mean Gaussian noise with standard deviation $0.1$. We consider $X_\mathrm{s}=[-1,1]$ and $X_0=[-0.25,0.25]$. Two different stochastic barrier functions are shown: (left) a 4th degree polynomial as synthesized via SoS optimization for a time horizon $H=10$ using the approach in santoyo2021barrier, and (right) the indicator function on the unsafe set for which $\beta=\int_{(\infty,-1]\cup [1,\infty]}\mathcal{N}(x\mid 1,0.1)dx$. We obtain a lower bound on $P_\mathrm{s}$ of $0.8275$ for SoS (left) and $0$ for the indicator function (right).
• Figure 2: We consider the same setting as in Fig.\ref{['fig:ex_1_and_3']} and for each state in the safe set, we plot upper and lower bounds of the probability of remaining within the safe set $[-1,1]$ for $10$ time steps starting from that state using two IMC abstractions: one obtained by discretizing the safe set uniformly with discretization step $dx=0.1$ and the other with $dx=0.02.$ For the initial set $X_0=[-0.25,0.25]$, we obtain a lower bound on $P_{\mathrm{s}}$ of $0.756$ for the case $dx=0.1$ (left) and $0.975$ for $dx=0.02$ (right).

Theorems & Definitions (22)

• Remark 1
• Definition 1: Policy
• Definition 2: Probabilistic Safety
• Remark 2
• Theorem 1
• Corollary 1
• Lemma 1
• Theorem 2: santoyo2021barrier
• Remark 3
• Remark 4