2025/11/02 by Hanna Krasowski, Dietrich, Elizabeth, Elizabeth Dietrich +10 · 1 citation
Computer Science · #Advanced Database Systems and Queries #Formal Methods in Verification #Interval temporal logic #Reachability #SIGNAL (programming language) #Semantic Web and Ontologies #Signal processing #Temporal logic #cs.LO #cs.RO
paper · pdf · doi:10.1109/lcsys.2026.3715556
published in IEEE Control Systems Letters, 1 (Institute of Electrical and Electronics Engineers)
openalex publication_date 2026/01/01 · openalex created_date 2026/07/22 · openalex updated_date 2026/08/01
Signal Temporal Logic (STL) is an expressive language for specifying behaviors of dynamical systems from continuous signals. However, a limitation of standard STL is its inherently deterministic semantics, which prevents it from accommodating uncertainty. Existing approaches to overcome this limitation are computationally costly and limit real-time capability, requiring repeated trajectory sampling or redesign of probability distributions over atomic propositions whenever the atomic propositions or specifications change. We introduce pacSTL, a framework that combines Probably Approximately Correct (PAC)-bounded reachable set predictions with an interval extension of STL. pacSTL computes lower and upper bounds on atomic robustness values by solving optimization problems over PAC-bounded reachable sets and propagates the bounds through the temporal logic operators. The resulting evaluation yields a PAC-bounded robustness interval at the specification level. We demonstrate the efficiency and relevance of pacSTL by verifying a quadrotor flight scenario and runtime monitoring a maritime navigation encounter.