Safety Verification of Nonlinear Stochastic Systems via Probabilistic Tube

作者：Zishun Liu, Saber Jafarpour, Yongxin Chen · 发表于：IEEE Transactions on Automatic Control · 年份：2026 · DOI：10.1109/tac.2026.3670756 · 被引用次数：3 · 研究领域：Formal Methods in Verification、Probabilistic and Robust Engineering Design、Fault Detection and Control Systems

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 strongly 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 b...