一句话：精确刻画 MTL 与 TPTL 在非负整数数据字上的路径检查复杂度，并导出确定性单计数器机模型检测的复杂度。
度量时序逻辑 MTL 与时间命题时序逻辑 TPTL 是线性时序逻辑的定量扩展，广泛用于实时系统验证。已有工作证明 MTL 在有限时间字上的路径检查属于 NC。本文将路径检查推广到非负整数上的无限数据字，这类字可视为单计数器机的行为。作者根据寄存器变量个数以及约束数采用一元或二进制编码，对 MTL 和 TPTL 路径检查问题进行了完整复杂度分析。主要结果：MTL 路径检查为 P-complete，TPTL 为 PSPACE-complete。由此得到确定性单计数器机针对 MTL/TPTL 公式模型检测的精确复杂度。
Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the path checking problem for MTL, when evaluated over finite timed words, is in the parallel complexity class NC. In this paper, we derive precise complexity results for the path-checking problem for MTL and TPTL when evaluated over infinite data words over the non-negative integers. Such words may be seen as the behaviours of one-counter machines. For this setting, we give a complete analysis of the complexity of the path-checking problem depending on the number of register variables and the encoding of constraint numbers (unary or binary). As the two main results, we prove that the path-checking problem for MTL is P-complete, whereas the path-checking problem for TPTL is PSPACE-complete. The results yield the precise complexity of model checking deterministic one-counter machines against formulae of MTL and TPTL.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FengLQ17,
title = {Path Checking for MTL and TPTL over Data Words},
author = {Shiguang Feng and Markus Lohrey and Karin Quaas},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:19)2017}
}