aiqbench analysis
pacSTL introduces a novel framework that integrates Probably Approximately Correct bounded reachable set predictions with Signal Temporal Logic to address uncertainty in dynamical systems. By solving optimization problems over these sets, the method efficiently computes robustness intervals for real-time verification without the computational overhead of repeated trajectory sampling. This advancement is particularly relevant for safety-critical applications like autonomous flight and maritime navigation where handling stochastic behavior within formal logic specifications is essential.
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
arXiv:2511.00934v3 Announce Type: replace-cross Abstract: 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.
Abstract: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.
Logic in Computer Science (cs.LO); Robotics (cs.RO)
arXiv:2511.00934 [cs.LO]
(or arXiv:2511.00934v3 [cs.LO] for this version)
https://doi.org/10.1109/LCSYS.2026.3715556 DOI(s) linking to related resources
Full text under the publisher's open licence · 167 words
Related coverage
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
arXiv · Jun 9, 2026
Article: The AI Productivity Paradox in Test Automation: Moving beyond Structural Validation to Perception and Intent
InfoQ · Jun 1, 2026
Article: Agentic Fitness Functions: Extending Evolutionary Architecture Beyond Deterministic Rules
InfoQ · Aug 17, 2026
Build durable agents with Temporal and Lakebase
Databricks · Sep 8, 2026