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

TL;DR

This paper introduces a novel reachability analysis framework that reduces uncertainty in verifying nonlinear systems against Signal Temporal Logic specifications, enabling precise, efficient, and adaptable system monitoring.

Contribution

It extends STL semantics with Boolean interval arithmetic and proposes an incremental reachability method to improve verification accuracy and efficiency under uncertainty.

Findings

Significant reduction in satisfaction ambiguity in case study

Enhanced precision in nested STL formula verification

Efficient uncertainty propagation and refinement

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.