定时监控性问题的时空分析

监控是验证工具箱中的重要组成部分，尤其是在使用模型检查等方法进行穷尽验证不可行的情况下。在线监控旨在基于有限的执行前缀在运行时确定规范的满足或违反。然而，并非所有规范都适合监控，例如没有有限执行可以证明满足或违反的属性。监控性问题即给定规范是否适合监控，已在离散时间中广泛研究。本文研究了由定时自动机表达的实时属性的监控性问题。对于由确定性定时 Muller 自动机给出的规范，我们证明了可判定性；而对于由非确定性定时 B"uchi 自动机给出的规范，我们指出该问题是不可判定的。此外，我们细化了监控性，还能确定在监控该属性前必须经过的事件数量以及时间。我们证明对于确定性定时 Muller 自动机，这些界限可以有效计算。相反，我们指出对于非确定性定时 B"uchi 自动机，这些界限不可计算。