数据字中MTL和TPTL的路径检查
摘要：度量时态逻辑（MTL）和定时命题时态逻辑（TPTL）是线性时态逻辑的定量扩展，被广泛用于实时系统的验证。最近的研究表明，在有限定时字中评估MTL的路径检查问题属于并行复杂性类NC。在本文中，我们推导出MTL和TPTL的路径检查问题在非负整数的无限数据字上的精确复杂性结果。此类字可以看作是单计数器机器的行为。对于这个设置，我们根据寄存器变量的数量和约束数的编码（一元或二元），给出了路径检查问题复杂性的完整分析。作为两个主要结果，我们证明了MTL的路径检查问题是P完全的，而TPTL的路径检查问题是PSPACE完全的。这些结果给出了针对MTL和TPTL公式对确定性单计数器机器进行模型检查的精确复杂性。
作者：Shiguang Feng, Markus Lohrey, Karin Quaas
论文ID：1412.3644
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22