艾伦关系的Meets与Started-by逻辑的模型检验是P^NP-完全的
计算机科学中的逻辑
2016-09-15 v1
摘要
在Halpern和Shoham的区间模态逻辑（HS）的众多片段中，由艾伦关系的Meets和Started-by构成的逻辑AB处于核心位置。诸如成就等仅在特定区间为真而在其任何子区间上不为真的陈述，以及关于区间长度的度量约束——例如强制区间至少（至多、恰好）为 k 点长——均可用AB表达。此外，在自然数 N 的线性序上，AB包含了（基于点的）逻辑LTL，因为它可以轻易编码next和until模态。最后，AB足以捕获ω-正则语言，即对每个ω-正则表达式R，存在一个AB公式φ，使得R定义的语言与φ在N上的模型集一致。已知AB在N上的可满足性问题是EXPSPACE-完全的。在此我们证明，在齐次性假设下，其模型检验问题是Δ^p_2 = P^NP-完全的（作为对比，全HS的模型检验问题是EXPSPACE-hard，且唯一已知的判定过程是非初等的）。此外，我们证明将艾伦关系Met-by模态添加到AB中不会带来额外代价（AA'B同样是P^NP-完全的）。
引用
@article{arxiv.1609.04090,
title = {Model Checking the Logic of Allen's Relations Meets and Started-by is $P^NP$-Complete},
author = {Laura Bozzelli and Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala},
journal= {arXiv preprint arXiv:1609.04090},
year = {2016}
}
备注
In Proceedings GandALF 2016, arXiv:1609.03648