Safety Verification of Nonlinear Stochastic Systems via Probabilistic Tube

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.