度量区间时态逻辑的一元片段：有界约束与下界约束（完整版）
计算机科学中的逻辑
2013-05-16 v1 形式语言与自动机理论
摘要
我们研究了著名的度量区间时态逻辑MITL[U_I,S_I]的两个一元片段，该逻辑最初由Alur和Henzinger提出，并确定了它们的表达能力和满足复杂性。我们证明，只有下界约束的一元模态的MITL[F_inf,P_inf]（令人惊讶地）对于偏序双向确定时间自动机（po2DTA）是表达完备的，并且从逻辑到自动机的归约给出了其NP完全的可满足性。我们还证明，只有有界区间的一元模态的片段MITL[F_b,P_b]具有NEXPTIME完全的可满足性。但奇怪的是，MITL[F_b,P_b]的表达能力严格弱于MITL[F_inf,P_inf]。我们提供了MITL各种一元片段可判定性和表达能力的全面图景。
引用
@article{arxiv.1305.3204,
title = {The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)},
author = {Paritosh K. Pandya and Simoni S. Shah},
journal= {arXiv preprint arXiv:1305.3204},
year = {2013}
}
备注
Presented at ATVA, 2012