A classic result by Stockmeyer gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of chop under the homogeneity assumption. In this paper, we study the complexity of the satisfiability problem for suitable weakenings of the chop interval temporal logic, that can be equivalently viewed as fragments of Halpern and Shoham interval logic. We first consider the logic $\mathsf{BD}_{hom}$ featuring modalities $B$, for \emph{begins}, corresponding to the prefix relation on pairs of intervals, and $D$, for \emph{during}, corresponding to the infix relation. The homogeneous models of $\mathsf{BD}_{hom}$ naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations. Such a fragment has been recently shown to be PSPACE-complete . In this paper, we study the extension $\mathsf{BD}_{hom}$ with the temporal neighborhood modality $A$ (corresponding to the Allen relation \emph{Meets}), and prove that it increases both its expressiveness and complexity. In particular, we show that the resulting logic $\mathsf{BDA}_{hom}$ is EXPSPACE-complete.

翻译：Stockmeyer的一个经典结果给出了星自由广义正则表达式的非空性问题的一个非初等下界。这一结果与区间时态逻辑的可满足性问题密切相关，特别是涉及所谓分割算子（chop operator）的公式。该算子可被解释为正则语言上连接运算的逆操作，而这种对应关系允许在星自由广义正则表达式的非空性问题与同质性假设下分割区间时态逻辑公式的可满足性问题之间建立归约。本文研究了分割区间时态逻辑的适当弱化版本的可满足性问题复杂度，这些版本可等价地视为Halpern与Shoham区间逻辑的子片段。我们首先考虑逻辑$\mathsf{BD}_{hom}$，其包含模态$B$（对应区间对的前缀关系）和$D$（对应区间对的中间关系）。$\mathsf{BD}_{hom}$的同质模型自然对应于由受限形式正则表达式定义的语言，这类表达式使用并、补以及前缀和中间关系的逆运算。该片段最近被证明是PSPACE完全的。本文进一步研究了加入时态邻域模态$A$（对应Allen关系中的"相遇"）的扩展逻辑$\mathsf{BD}_{hom}$，并证明该扩展同时提升了其表达能力和复杂度。特别地，我们证明由此得到的逻辑$\mathsf{BDA}_{hom}$是EXPSPACE完全的。