Safety Verification of Stochastic Systems: A Set-Erosion Approach

TL;DR

An approach for safety verification termed set-erosion strategy that verifies the safety of a stochastic system on a safe set through the safety of its associated deterministic system on an eroded subset is proposed.

Abstract

We study the safety verification problem for discrete-time stochastic systems. We propose an approach for safety verification termed set-erosion strategy that verifies the safety of a stochastic system on a safe set through the safety of its associated deterministic system on an eroded subset. The amount of erosion is captured by the probabilistic bound on the distance between stochastic trajectories and their associated deterministic counterpart. Building on our recent work [1], we establish a sharp probabilistic bound on this distance. Combining this bound with the set-erosion strategy, we establish a general framework for the safety verification of stochastic systems. Our method is flexible and can work effectively with any deterministic safety verification techniques. We exemplify our method by incorporating barrier functions designed for deterministic safety verification, obtaining barrier certificates much tighter than existing results. Numerical experiments are conducted to demonstrate the efficacy and superiority of our method.

Figures (3)

• Figure 1: An illustration of set-erosion strategy. Here $\mathcal{C}$ in green is the safe set, and the blue area is the eroded subset $\mathcal{C}\ominus\mathcal{B}^n\left(r_{\delta,t},0\right)$ with $r_{\delta,t}$ given in Theorem \ref{['thm: set-erosion']}-2). By Theorem \ref{['thm: set-erosion']}, if the deterministic trajectory stays in the blue area at any time, then the stochastic trajectory is safe on $\mathcal{C}$ with $1-\delta$ guarantee.
• Figure 2: The probability $\underline{\delta}$ (the lower the safer) that a strategy cannot guarantee safety on the centered ball with radius $R$ during $t\leq T$. The blue curve is given by our strategy \ref{['eq: delta>=']}, the yellow curve is the simulated result from $3\times10^6$ sampled trajectories, and the red curve is the baseline we choose, given by the main result of cosner2024bounding. Left:$T=100$. Right:$T=200$.
• Figure 3: Stochastic safety verification of the unicycle system \ref{['sys: uni']} with $1-10^{-4}$ failure guarantee. Left: Stochastic safety verification using the set-erosion strategy at the terminal time $T=100,500$. The red shapes are obstacles. The yellow areas are the eroded part $\mathcal{C}\backslash(\mathcal{C}\ominus\mathcal{B}^n\left(r_m,0\right))$. Each curve is an independent trajectory of the associated deterministic unicycle system with different $d_t$. Right: Simulation of the stochastic trajectories. Each curve is an independently sampled trajectory of the stochastic system \ref{['sys: uni']} during $t\leq T$, $T=100,500$.

Theorems & Definitions (14)

• Definition II.1: sub-Gaussian
• Definition II.2
• Theorem 1: Set-erosion strategy
• proof
• Proposition 1: Stochastic deviation szy2024Auto
• Remark IV.1
• Theorem 2: Stochastic trajectory gap
• proof
• Definition V.1: TV-RBF
• Proposition 2