一句话：证明齐性假设下区间时序逻辑 BE 的有限可满足问题是 ExpSpace 完全的。
本文研究齐性假设下区间时序逻辑 BE 的有限可满足性问题。BE 是 Halpern–Shoham 区间时序逻辑的核心片段，其模态算子分别对应区间的前缀（Begins）和后缀（Ends）关系，复杂度介于非初等的 Chop 逻辑 C 与 PSpace 完全的 D 逻辑之间。此前 BE 已知 ExpSpace 难，且唯一可满足性过程是原始递归但非初等。作者证明 BE 的有限可满足性是 ExpSpace 完全的：构造一个等可满足的范式，使嵌套模态数目有界；该归一化技术类似 Scott 的量词消去，但因齐性假设限制而更复杂。
In this paper, we study the finite satisfiability problem for the logic BE under the homogeneity assumption. BE is the cornerstone of Halpern and Shoham’s interval temporal logic, and features modal operators corresponding to the prefix (a.k.a. "Begins") and suffix (a.k.a. "Ends") relations on intervals. In terms of complexity, BE lies in between the "Chop" logic C, whose satisfiability problem is known to be non-elementary, and the PSpace-complete interval logic D of the sub-interval (a.k.a. "During") relation. BE was shown to be ExpSpace-hard, and the only known satisfiability procedure is primitive recursive, but not elementary. Our contribution consists of tightening the complexity bounds of the satisfiability problem for BE, by proving it to be ExpSpace-complete. We do so by devising an equi-satisfiable normal form with boundedly many nested modalities. The normalization technique resembles Scott’s quantifier elimination, but it turns out to be much more involved due to the limitations enforced by the homogeneity assumption.
@inproceedings{MonicaMPS23,
title = {The Logic of Prefixes and Suffixes is Elementary under Homogeneity<sup>*</sup>},
author = {Dario Della Monica and Angelo Montanari and Gabriele Puppis and Pietro Sala},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175824}
}