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 the 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 specification.

翻译：信号时序逻辑（STL）是一种用于描述连续信号中动态系统行为的表达性语言。然而，标准STL的局限性在于其固有确定性语义，无法适应不确定性。现有克服此局限的方法计算成本高昂，且限制了实时能力——每当原子命题或规范变更时，需重复进行轨迹采样或重新设计原子命题上的概率分布。我们提出pacSTL框架，该框架将概率近似正确（PAC）有界可达集预测与STL的区间扩展相结合。pacSTL通过求解PAC有界可达集上的优化问题，计算原子鲁棒性的上下界，并通过时序逻辑算子传播这些界。最终评估在规范层面得到PAC有界鲁棒性区间。我们通过验证四旋翼飞行场景和运行时监测航海导航规范，展示了pacSTL的效率与实用性。