无自动机的运行时监控通过轨迹检查（扩展版）
形式语言与自动机理论
2025-11-17 v1 计算机科学中的逻辑
摘要
在运行时验证中，监控由分析系统当前执行并根据观察到的有限轨迹来确定，所有可能的续续是否满足或违反给定规范。这通常通过从以线性时间逻辑 (LTL) 或其有限词变体 (LTLf) 表达的逻辑规范合成监控器--通常是确定性有限状态自动机 (DFA)--来完成。不幸的是， resulting DFA 的大小可能在公式大小上导致双指数级膨胀。本文我们识别了一些在不构造此类 DFA 的情况下进行监控的条件。我们建立在 [Kupferman & Vardi, FMSD, 2001] 引入的有意安全和 cosafe 公式概念基础上，展示了通过轨迹检查（即直接在当前系统轨迹上对其进行评估）可以实现监控，这在公式和轨迹大小上具有多项式复杂度。此外，我们研究了识别有意安全和 cosafe 公式的复杂度，这些公式属于 LTL 和 LTLf 的 safety 和 cosafety 片段。对于 LTLf，我们显示，这些片段中的所有公式都是 intentionally safe and cosafe，从而消除了检查的需要。对于 LTL，我们证明了该问题在 PSPACE 中，显著优于 full LTL 的 EXPSPACE 复杂度。
引用
@article{arxiv.2511.11072,
title = {Automata-less Monitoring via Trace-Checking (Extended Version)},
author = {Andrea Brunello and Luca Geatti and Angelo Montanari and Nicola Saccomanno},
journal= {arXiv preprint arXiv:2511.11072},
year = {2025}
}