Uncertainty Removal in Verification of Nonlinear Systems against Signal Temporal Logic via Incremental Reachability Analysis

TL;DR

The paper tackles uncertainty in verifying STL properties for nonlinear continuous-time systems by integrating reachability analysis with Boolean interval arithmetic. It introduces a unitary-signal framework and a marker-based uncertainty tracking mechanism that distinguishes whether indeterminacy arises from over-approximation or incomplete simulations, enabling selective refinement of only the relevant reachable sets. The approach supports both offline and online monitoring and contracts/refines the reachable tube adaptively to improve precision while avoiding unnecessary recomputation. A nonlinear oscillator case study demonstrates substantial reductions in satisfaction ambiguity and favorable computational performance compared with baseline methods.

Abstract

A framework is presented for the verification of Signal Temporal Logic (STL) specifications over continuous-time nonlinear systems under uncertainty. Based on reachability analysis, the proposed method addresses indeterminate satisfaction caused by over-approximated reachable sets or incomplete simulations. STL semantics is extended via Boolean interval arithmetic, enabling the decomposition of satisfaction signals into unitary components with traceable uncertainty markers. These are propagated through the satisfaction tree, supporting precise identification even in nested formulas. To improve efficiency, only the reachable sets contributing to uncertainty are refined, identified through the associated markers. The framework allows online or offline monitoring to adapt to incremental system evolution while avoiding unnecessary recomputation. A case study on a nonlinear oscillator demonstrates a significant reduction in satisfaction ambiguity, highlighting the effectiveness of the approach.

Figures (6)

• Figure 1: Satisfaction tree maler_monitoring_2004 and associated satisfaction signals.
• Figure 2: Unitary signal decomposition of $[\mathcal{S}_{\phi_1}](t)$ in $\phi_1 U_{[a,b]} \phi_2$; uncertainty indices in orange.
• Figure 3: Uncertainty tracking in the $\vee$ operation between two satisfaction signal (in color) using unitary signals; uncertainty indices in orange.
• Figure 4: Time bisection and contraction, $\mathcal{X}_\mu$ a set predicate.
• Figure 5: Initial tube on the left and refined tube on the right.

Theorems & Definitions (14)

• Definition 1
• Definition 2
• Definition 3: satisfaction signal maler_monitoring_2004Lercher2024CAV
• Definition 4: unitary decomposition maler_monitoring_2004
• Definition 5
• Lemma 1: unitary decomposition of $U_{[a,b]}$ maler_monitoring_2004
• Definition 6: Boolean interval arithmetic kearfott_logical_2019jaulin_applied_2001
• Definition 7: set-based extension of predicate Tillet2025ActaCyberneticaLercher2024CAV
• Definition 8: uncertain and certain unitary signals
• Definition 9: uncertain unitary decomposition