Safety Verification of Nonlinear Stochastic Systems via Probabilistic Tube

TL;DR

This work tackles safety verification for nonlinear stochastic systems by decoupling stochastic disturbances from deterministic dynamics using a set-erosion strategy. Central to the approach is a probabilistic tube (PT) that bounds the deviation between stochastic trajectories and their associated deterministic trajectories through an affine-martingale (AM) framework based on the Averaged Moment Generating Function (AMGF), yielding a tight, non-asymptotic bound that scales like $\mathcal{O}(\sqrt{\log(1/\delta)})$. The PT enables reducing stochastic safety verification to deterministic safety checks on an eroded safe set and is extended to both continuous-time (CT) and discrete-time (DT) systems, with refinements for contractive dynamics via union bounds. The framework is demonstrated on reachability-based safety verification and safe controller synthesis, including a unicycle and a nonlinear mass-spring-damper chain, illustrating practical applicability to robotics and autonomous systems. The results provide a scalable, probabilistic guarantee mechanism that pairs rigorous theory with deterministic verification tools.

Abstract

We address the problem of safety verification for nonlinear stochastic systems, specifically the task of certifying that system trajectories remain within a safe set with high probability. To tackle this challenge, we adopt a set-erosion strategy, which decouples the effects of stochastic disturbances from deterministic dynamics. This approach converts the stochastic safety verification problem on a safe set into a deterministic safety verification problem on an eroded subset of the safe set. The success of this strategy hinges on the depth of erosion, which is determined by a probabilistic tube that bounds the deviation of stochastic trajectories from their corresponding deterministic trajectories. Our main contribution is the establishment of a tight bound for the probabilistic tube of nonlinear stochastic systems. To obtain a probabilistic bound for stochastic trajectories, we adopt a martingale-based approach. The core innovation lies in the design of a novel energy function associated with the averaged moment generating function, which forms an affine martingale, a generalization of the traditional c-martingale. Using this energy function, we derive a precise bound for the probabilistic tube. Furthermore, we enhance this bound by incorporating the union-bound inequality for strictly contractive dynamics. By integrating the derived probabilistic tubes into the set-erosion strategy, we demonstrate that the safety verification problem for nonlinear stochastic systems can be reduced to a deterministic safety verification problem. Our theoretical results are validated through applications in reachability-based safety verification and safe controller synthesis, accompanied by several numerical examples that illustrate their effectiveness.

Figures (9)

• Figure 1: An illustration of set-erosion strategy and probabilistic tube. (a):$\mathcal{C}$ between the walls is the safe set, and the aisle between the blue areas is the eroded subset $\mathcal{C}\ominus\mathcal{B}^n\left(r_{\delta,t},0\right)$ with $r_{\delta,t}$ defined in Definition \ref{['def: PT']}. By Theorem \ref{['thm: set-erosion']}, if the deterministic trajectory stays in the white aisle at any time, then the stochastic trajectory is safe on $\mathcal{C}$ with $1-\delta$ guarantee. (b): Probabilistic tube (PT). The black solid line is the deterministic trajectory $x_t$, and the stochastic trajectories $X_t$ are associated to it. Tubes in different colors are PTs with different probability level $\delta$.
• Figure 2: Figures of trajectories $\|X_t\|$ of the linear system \ref{['sys: lin']} . Each figure contains 5000 independent trajectories and the $r_{\delta,t}$ calculated by \ref{['eq: r CT']} with $\delta=10^{-3}$ and $\varepsilon=1/16$, but under different $c$ and $T$.
• Figure 3: The strategy of modifying PT for contractive systems. The black dashed line is the probabilistic bound \ref{['eq: prop1']} on stochastic deviation, the short red curves are the bound \ref{['eq: r CT']} on PT over a short time window, and the blue dashed line is the modified PT.
• Figure 4: Comparison of the PT for linear system \ref{['sys: lin']} with $c=-0.5$. Left: the red dashed curve is the bound $r_{\delta,t}$ in Theorem \ref{['thm: CT bound']}. Right: the blue solid curve is the bound $r_{\delta,t}$ in Theorem \ref{['thm: improved CT bound']} with $\Delta t=0.05$. Each figure contains 5000 independent trajectories of $\|X_t-x_t\|$ (with $x_t\equiv0$), and use $\delta=0.001$, $\varepsilon=1/16$.
• Figure 5: The bound $r_{\delta,t}$ from Theorem \ref{['thm: improved CT bound']} with different $\Delta t$. Left: $r_{\delta,t}$ with four different choices of $\Delta t$ over $t\in[0,5]$, Right: $r_{\delta,t}$ with $\Delta t\in[10^{-4},0.3]$ at different time $t$.

Theorems & Definitions (23)

• Definition 2.1: Matrix Measure
• Definition 2.2: sub-Gaussian
• Definition 3.1: Probabilistic Tube
• Theorem 1: Set-erosion strategy
• Proposition 1
• Remark 3.1
• Proposition 2
• Proposition 3
• Definition 4.1: CT Affine Martingale
• Lemma 4.1