pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis

TL;DR

pacSTL addresses uncertainty in safety specifications by combining PAC-bounded reachable tubes with an interval extension of STL to produce robustness intervals $[\underline{h}, \overline{h}]^\phi$ with probabilistic guarantees. It decouples dynamics and environment via data-driven reachability and derives PAC guarantees for both atomic propositions and the full specification, enabling robust monitoring even as atomic predicates change (e.g., COLREGS-based maritime rules). The framework supports convex representations (e.g., $\mathcal{E}$, $\mathcal{Z}$) and provides time-point tracking to relate bounds to specific trajectory milestones, demonstrated through simulation and real-world experiments with model vessels. This approach offers provable, real-time capable monitoring for autonomous systems operating under uncertainty, with applicability to diverse domains beyond maritime navigation.

Abstract

Real-world robotic systems must comply with safety requirements in the presence of uncertainty. To define and measure requirement adherence, Signal Temporal Logic (STL) offers a mathematically rigorous and expressive language. However, standard STL cannot account for uncertainty. We address this problem by presenting pacSTL, a framework that combines Probably Approximately Correct (PAC) bounded set predictions with an interval extension of STL through optimization problems on the atomic proposition level. pacSTL provides PAC-bounded robustness intervals on the specification level that can be utilized in monitoring. We demonstrate the effectiveness of this approach through maritime navigation and analyze the efficiency and scalability of pacSTL through simulation and real-world experimentation on model vessels.

Figures (9)

• Figure 1: Example evaluation of a PAC-bounded Signal Temporal Logic (pacSTL) specification $\phi$, which is based on the example atomic proposition $\mathtt{encounter}$. The robustness intervals for this atomic proposition $h_\mathtt{encounter}$ are computed based on convex optimization. The reachable tube $\mathcal{R}$ and its accuracy are calculated through scenario optimization. The result is a probabilistic guarantee on the containment of an unseen system trajectory in the robustness interval of $\phi$, here $[-1.0, 2.4]$.
• Figure 2: Proposed pacSTL framework that combines PAC-bounded reachable tubes and optimization problems for lower and upper atomic robustness bounds to achieve robustness intervals and probabilistic guarantees for pacSTL specifications.
• Figure 3: Duffing Oscillator in $\mathbb{R}^2$ with reachable set estimates as an ellipsoid $\mathcal{E}$ (gold), a zonotope with 4 generators $\mathcal{Z}_1$ (dark pink), and a zonotope with 2 generators $\mathcal{Z}_2$ (light pink).
• Figure 4: Minimal example of robustness bound calculations given PAC-bounded ellipsoid reachable sets for three time steps and varying atomic robustness functions in state space $\mathcal{X}$. The lines are where the robustness functions equal zero, i.e., $h_i(x)=a_i^\top x + b _i = 0$. The colors indicate different time steps, while $+$ and $-$ denote which side corresponds to satisfaction and falsification, respectively.
• Figure 5: Reachable tubes for 5 time steps with time step size 0.5s, increasingly opaque for later time steps. Left: Reachable tubes projected to the position domain, i.e., $p_x$ and $p_y$. Right: Reachable tubes projected to $\psi$ and $vel$.

Theorems & Definitions (12)

• Theorem 1: Adapted from Thm. 1, dietrich2025datadrivenreachabilityscenariooptimization
• Definition 1: Ellipsoids
• Definition 2: Zonotopes
• Lemma 1
• proof
• Corollary 1: Adapted from Baird2023, Thm. 1 and Def. 5
• proof
• Theorem 2: Reachable Tube pacSTL
• proof
• Definition 3