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算子的公式）的可满足性问题密切相关。该算子可被解释为正则语言上连接操作的逆运算，这种对应关系使得在齐次性假设下，星自由广义正则表达式的非空性问题与chop区间时态逻辑公式的可满足性问题之间能够进行归约。本文研究了适合chop区间时态逻辑弱化版本的可满足性问题的复杂度，这些版本可等价地视为Halpern和Shoham区间逻辑的子片段。我们首先考虑逻辑$\mathsf{BD}_{hom}$，其包含模态$B$（表示"开始"，对应区间对的前缀关系）和$D$（表示"期间"，对应中缀关系）。$\mathsf{BD}_{hom}$的齐次模型自然对应由受限正则表达式（使用并、补以及前缀和中缀关系的逆）定义的语言。该片段最近已被证明是PSPACE完全的。本文研究了$\mathsf{BD}_{hom}$在添加时间邻域模态$A$（对应Allen关系"相遇"）后的扩展，并证明该扩展同时提升了其表达能力和复杂度。特别地，我们证明由此得到的逻辑$\mathsf{BDA}_{hom}$是EXPSPACE完全的。