在前缀和中缀的时间逻辑中加入关系满足使之成为EXPSPACE-完备的
Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete
摘要：
在表达性和复杂性之间选择正确的折衷是区间时态逻辑的主要问题。在他们的开创性论文中，Halpern和Shoham表明HS（艾伦关系的时序逻辑）的可满足性问题在任何合理的线性序类上都是高度不可判定的。为了恢复可判定性，可以限制时间模态的集合和/或模型的类别。在下文中，我们专注于HS片段在同质性假设下的可满足性问题，根据该假设，任何命题字母在区间上成立，如果它在所有点上成立。具有齐次性的完全HS问题已经被证明是非初等可判定的，但它唯一已知的下界是EXPSPACE（事实上，对于前缀和后缀BE的逻辑已经证明了EXPSPACE-困难，这是它的一个非常小的片段。本文证明了将Allen关系Meets加到BD上使BD成为EXPSPACE完备的。
英文摘要：
The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper, Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) is highly undecidable over any reasonable class of linear orders. In order to recover decidability, one can restrict the set of temporal modalities and/or the class of models. In the following, we focus on the satisfiability problem for HS fragments under the homogeneity assumption, according to which any proposition letter holds over an interval if only if it holds at all its points. The problem for full HS with homogeneity has been shown to be non-elementarily decidable, but its only known lower bound is EXPSPACE (in fact, EXPSPACE-hardness has been shown for the logic of prefixes and suffixes BE, which is a very small fragment of it. The logic of prefixes and infixes BD has been recently shown to be PSPACE-complete. In this paper, we prove that the addition of the Allen relation Meets to BD makes it EXPSPACE-complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
