TY - GEN
T1 - Uncertainty Removal in Verification of Nonlinear Systems against Signal Temporal Logic via Incremental Reachability Analysis
AU - Besset, Antoine
AU - Tillet, Joris
AU - Dit Sandretto, Julien Alexandre
N1 - Publisher Copyright:
© 2025 IEEE.
PY - 2025/1/1
Y1 - 2025/1/1
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/105031909576
U2 - 10.1109/CDC57313.2025.11312035
DO - 10.1109/CDC57313.2025.11312035
M3 - Conference contribution
AN - SCOPUS:105031909576
T3 - Proceedings of the IEEE Conference on Decision and Control
SP - 6400
EP - 6407
BT - 2025 IEEE 64th Conference on Decision and Control, CDC 2025
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 64th IEEE Conference on Decision and Control, CDC 2025
Y2 - 9 December 2025 through 12 December 2025
ER -