Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications

TL;DR

The paper tackles verifying safety specifications expressed in Signal Temporal Logic (STL) for nonlinear discrete-time stochastic systems under both bounded disturbances and stochastic noise. The authors introduce an STL erosion strategy that tightens each predicate’s region of interest using a probabilistic reachable set, turning probabilistic STL satisfaction into a deterministic STL verification problem against a tightened formula. A key contribution is a rigorous bound on stochastic trajectory deviation that enables constructing tight PRSs and guarantees of the form $\mathbb{P}(\boldsymbol{X}_{[0,T]} \models \varphi) \ge 1-\delta$ by verifying $\tilde{\varphi}$ for the associated deterministic system. The approach is compatible with existing deterministic STL verifiers and demonstrated on a linear double-integrator and a nonlinear unicycle, showing reduced conservativeness compared with worst-case analyses and practical applicability to real-world safety-critical systems. This work advances safe verification in stochastic settings and lays groundwork for future control synthesis under probabilistic STL constraints.

Abstract

We study the verification problem of stochastic systems under signal temporal logic (STL) specifications. We propose a novel approach that enables the verification of the probabilistic satisfaction of STL specifications for nonlinear systems subject to both bounded deterministic disturbances and stochastic disturbances. Our method, referred to as the STL erosion strategy, reduces the probabilistic verification problem into a deterministic verification problem with a tighter STL specification. The degree of tightening is determined by leveraging recent results on bounding the deviation between the stochastic trajectory and the deterministic trajectory. Our approach can be seamlessly integrated with any existing deterministic STL verification algorithm. Numerical experiments are conducted to showcase the efficacy of our method.

Figures (3)

• Figure 1: An illustration of the STL erosion method. Here we consider a simple STL specification: $\varphi:=\square_{[t_1,t_2]}\pi$, where the super level set of the predicate $\pi$ is $\mathcal{C}$. This STL specification requires the state to remain inside a safe set $\mathcal{C}$ from $t_1$ to $t_2$. The predicate $\pi$ is eroded by $\tilde{E}$. If the deterministic trajectory can satisfy the tightened STL formula $\tilde{\varphi} = \square_{[t_1,t_2]}\tilde{\pi}$, then the stochastic trajectory would satisfy $\varphi$ with a high probability.
• Figure 2: Stochastic STL verification of the double integrator system \ref{['eq: double integrator']} with $1-10^{-4}$ guarantee. Left: Stochastic STL verification using our STL erosion strategy. The gray circle and the green circle represent the obstacle and the goal area respectively. The corresponding eroded predicates are represented as yellow areas. Each curve is an independent trajectory of the deterministic system. Right: Each curve is an independent trajectory of the stochastic system.
• Figure 3: Stochastic STL verification of the unicycle system with $1-10^{-4}$ guarantee. Left: Stochastic STL verification using our STL erosion strategy. The blue circle represents the first goal area. The green circle represents the second goal area. The red hexagon is the obstacle. The corresponding eroded predicates are represented as yellow areas. Each curve is an independent trajectory of the deterministic system. Right: Each curve is an independent trajectory of the stochastic system.

Theorems & Definitions (15)

• Definition 1
• Definition 2
• Definition 3
• Remark 1
• Definition 4
• Definition 5: PRS
• Proposition 1: Predicate erosion
• proof
• Theorem 1: STL formula erosion
• proof