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 的经典结果 { stockmeyer 的经典结果 { 将无恒星通用常规表达式的平坦性问题置于非元素下下限 { 平坦常规表达式的平坦性问题 。 此结果与使用所谓的切片操作器的公式的静坐性问题密切相关, 特别是使用所谓的切片操作器的公式。 这样的操作者可以被解读为常规语言的交接操作的反向, 而这种对等使得无恒星通用常规表达式的不纯度和对等公式在平流假设下的切片间时间逻辑值。 在本文中, 我们研究的静坐性问题的复杂性, 与切片时间逻辑值和Shom 时间逻辑逻辑的折合性问题。 我们的平流式模型显示的是 美元的平流化模式 。