The addition of temporal neighborhood makes the logic of prefixes and sub-intervals EXPSPACE-complete

TL;DR

This work characterizes the impact of adding the right-endpoint modality A to the BD_{hom} fragment of Halpern–Shoham interval logic, yielding the fragment BDA_{hom}. Using homogeneous compass structures and a sequence of spatial invariants (columns, rows, and equivalence classes), it derives a small-model property and an EXPSPACE decision procedure for BD_{hom}, then extends the framework to BDA_{hom} with matching EXPSPACE complexity. The key results are that BD_{hom} is in EXPSPACE and that BDA_{hom} is EXPSPACE-complete, achieved via a unified, model-theoretic approach that also supports a hardness proof through a TM-space reduction. This advances understanding of how adding endpoint-sensitive operators escalates complexity in interval temporal logics under homogeneity, and it lays groundwork for analyzing related HS_{hom} fragments and potential model-checking applications.

Abstract

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.

Figures (22)

• Figure 1: Point-based ($\pi$) vs. interval-based ($\mathcal{V}$) labelling over the same finite linear order.
• Figure 2: The semantics of the three $\mathsf{CDT}$ binary modalities $\mathsf{C}$, $\mathsf{D}$, and $\mathsf{T}$.
• Figure 3: Allen's relations and the corresponding $\mathsf{HS}$ modalities (the relations/modalities considered in this work are highlighted).
• Figure 4: The encoding of $\mathrm{LTL}_f$ modalities $\ \mathrm{U}\ $ and $\varbigcirc$ in $\mathrm{AB}$.
• Figure 5: A homogeneous model (a - left) vs. a general one (b - right).

Theorems & Definitions (55)

• Definition 3.1: Homogeneity
• Example 3.2
• Definition 4.1
• Definition 4.2
• Example 4.3
• Definition 4.4
• Example 4.5
• Proposition 4.5
• Example 4.6
• Proposition 4.7