带值冻结算子的信号时序逻辑 (STL*) 的快速鲁棒监控

Bassem Ghorbel; Vinayak S. Prabhu

带值冻结算子的信号时序逻辑 (STL*) 的快速鲁棒监控

计算机科学中的逻辑 2024-10-01 v2 系统与控制系统与控制

作者: Bassem Ghorbel , Vinayak S. Prabhu

摘要

此前，研究者提出在信号时序逻辑 (STL) 中引入值冻结算子，以表达 STL 无法表达的工程性质。这种增强逻辑被称为 STL*。此前 STL* 的监控算法不可扩展，且无法处理嵌套冻结变量。我们提出了离线离散时间监控算法及加速启发式方法，适用于布尔监控和定量鲁棒性监控。该加速启发式在子公式为真的时间区间上操作，而非在原始轨迹采样点上操作。我们对算法进行了实验验证，结果表明算法能够监控包含两个或三个嵌套冻结变量的长轨迹。本文工作是首个针对含嵌套冻结变量的 STL* 公式的监控算法实现。

关键词

信号时序逻辑值冻结算子 STL* 监控算法布尔监控定量鲁棒性嵌套冻结变量加速启发式

引用

@article{arxiv.2408.02460,
  title  = {Fast Robust Monitoring for Signal Temporal Logic with Value Freezing Operators (STL*)},
  author = {Bassem Ghorbel and Vinayak S. Prabhu},
  journal= {arXiv preprint arXiv:2408.02460},
  year   = {2024}
}

备注

Full version of MEMOCODE 2024 paper

带值冻结算子的信号时序逻辑 (STL*) 的快速鲁棒监控

摘要

关键词

引用

备注

相关论文