用概率保证的可达集提升时序逻辑的不确定性处理能力。
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
- 结合PAC可达集与区间扩展时序逻辑，量化不确定系统的性质验证。
- 在四轴飞行器和海上航行场景中实现高效实时验证与监控。
- 适合关注动态系统安全验证的工程与算法研究者。
信号时序逻辑（STL）是描述动态系统连续信号行为的强大语言，但其固有的确定性语义无法处理不确定性。现有方法计算成本高，难以实现实时性，需频繁重采轨迹或重新设计原子命题的概率分布。本文提出pacSTL框架，将概率近似正确（PAC）可达集预测与STL的区间扩展相结合。通过在PAC可达集上求解优化问题，计算原子鲁棒性的上下界，并沿时序逻辑算子传播，最终得到规范级别的PAC有界鲁棒区间。在四轴飞行器飞行场景中验证了该方法的效率与适用性，并实现了对海上航行相遇事件的运行时监控。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。