On Coarser Interval Temporal Logics and their Satisfiability Problem

Abstract

The primary characteristic of interval temporal logic is that intervals, rather than points, are taken as the primitive ontological entities. Their computational behaviour is generally bad, and several restrictions have been considered in order to define decidable and computationally affordable temporal logics based on intervals. In this paper we take inspiration from Golumbic and Shamir’s coarser interval algebras, which generalize the classical Allen’s Interval Algebra, in order to define two previously unknown variants of Halpern and Shoham’s logic ($\mathrm{HS}$). We prove that one of them (denoted here by $\mathrm{HS_7}$) is still generally undecidable, while the other one ($\mathrm{HS_3}$) becomes, perhaps surprisingly, PSpace-complete, at least in the finite case.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Time intervals, rather than time points, are regarded in interval temporal logics as the primitive ontological entities, and the truth of formulae is defined accordingly. These logics can be applied in many fields, such as hardware and real-time system verification, language processing, constraint satisfaction and planning, among others [1, 12, 20, 21]. Moreover, interval temporal logics have been considered as the basis for temporal extensions of Description Logic [2–4, 22]. The most influential interval temporal logic is probably Halpern and Shoham’s Modal Logic of Allen’s Relations ($\mathrm{HS}$) [15], and it is well-known that the satisfiability problem for $\mathrm{HS}$, interpreted over most interesting classes of linearly ordered sets is (highly) undecidable.

The different strategies that have been used to obtain fragments of $\mathrm{HS}$ that perform better can be summarized as follows: (i) limiting the set of modalities that are included in the language; (ii) interpreting the language over semantically incomplete linear structures; (iii) limiting the nesting of temporal modalities; (iv) restricting the applicability of boolean operators and/or relaxing the semantics of the modal operators. The few fragments or variants of $\mathrm{HS}$ that have been proven to be decidable show complexities that range from NP-complete to NExpTime-complete, ExpSpace-complete, and even non-primitive recursive; undecidability is still the rule even when sub-propositional fragments are considered [7–11, 18].

Allen’s Interval Algebra (IA) [1] can be seen as the backbone of $\mathrm{HS}$: modal operators in the $\mathrm{HS}$ repository can be mapped one-by-one over Allen’s interval relations. In [14] Golumbic and Shamir propose to reduce the set of binary relations between intervals by defining coarser relations that correspond to logical disjunctions of Allen’s relations. In this way, two natural coarser algebras emerge, namely IA$_7$ and IA$_3$. The former encompasses seven relations, by preserving the original relations before,after, and equal to, by joining meets and overlaps into a single relation (and similarly for their inverse ones), and by joining during, starts, and finishes into a single relation (and, again, similarly for their inverse ones). The latter encompasses only three relations: the original before and after, plus a relation (intersects) that can be viewed as the disjunction of all the remaining ones (and therefore is the inverse of itself and includes equality). In this work we propose two fragments of $\mathrm{HS}$ based on the same idea: $\mathrm{HS_7}$ retains from $\mathrm{HS}$ the modal operators that correspond to before and after, and includes new ones corresponding each to one of the relations of IA$_7$, except equality; similarly, $\mathrm{HS_3}$ features three modal operators, one for each of $\hbox {IA}_3$’s binary relation. These logics can be naturally applied to the same fields as full $\mathrm{HS}$; moreover they reflect the idea underlying the standard SQL:2011 [16], where interval relations are not necessarily Allen’s ones (for example, later is interpreted as the disjunction of Allen’s meets and later). We prove here that while (not surprisingly) $\mathrm{HS_7}$ is still undecidable when interpreted over every interesting class of linearly ordered sets, $\mathrm{HS_3}$ becomes PSpace-complete at least in the finite case. Given the generally bad computational behaviour of interval logics (e.g., in the universe of the syntactical fragments of $\mathrm{HS}$, the decidable ones account for around $10\,\%$ of the expressively different ones - see, for example, [7]) this result strikes out as an interesting exception. While the PSpace-hardness of $\mathrm{HS_3}$ holds in all considered cases, its decidability in the infinite cases is an open problem, although our exploratory analysis suggests that PSpace-membership of $\mathrm{HS_3}$ in the finite case should be transferrable to the infinite cases as well.

2 Preliminaries

Let $\mathbb {D} = \langle D, <\rangle$ be a strict (i.e., irreflexive) linearly ordered set. A strict interval (resp., non-strict interval) over $\mathbb {D}$ is an ordered pair [x, y], where $x,y \in D$ and $x < y$ (resp., $x\le y$). In the recent literature, the strict semantics, where only strict intervals are considered, is usually adopted. This conforms to the definition of interval adopted by Allen in [1], but differs from the one given by Halpern and Shoham in [15]. If we exclude the identity relation, there are 12 different relations between two intervals in a linear order, often called Allen’s relations [1]: the six relations $R_A$ (adjacent to), $R_L$ (later than), $R_B$ (begins), $R_E$ (ends), $R_D$ (during), and $R_O$ (overlaps), depicted in Fig. 1, and their inverses, that is, $R_{\overline{X}} = (R_{X})^{-1}$, for each $X \in \{ A, L, B, E, D, O \}$. We interpret interval structures as Kripke structures, with Allen’s relations playing the role of the accessibility relations. Thus, we associate a universal modality [X] and an existential modality $\langle X\rangle$ with each Allen relation $R_{X}$. For each $X \in \{ A, L, B, E, D, O \}$, the transposes of the modalities [X] and $\langle X \rangle$ are the modalities $[\overline{X}]$ and $\langle \overline{X} \rangle$, corresponding to the inverse relation $R_{\overline{X}}$ of $R_{X}$. Halpern and Shoham’s logic $\mathrm{HS}$ [15] is a multi-modal logic with formulae built from a finite, non-empty set $\mathcal {AP}$ of atomic propositions (also referred to as proposition letters), the classical propositional connectives, and a pair of modalities for each Allen relation:

$$\begin{aligned} \varphi :\!{:}\!= \bot \,\,|\,\,p \,\,|\,\,\lnot \varphi \,\,|\,\,\varphi \vee \varphi \,\,|\,\,\varphi \wedge \varphi \,\,|\,\,\langle X \rangle \varphi \,\,|\,\,\langle \overline{X} \rangle \varphi , \end{aligned}$$

where $p \in \mathcal {AP}$ and $X \in \{ A, L, B, E, D, O \}$. The other propositional connectives and constants (e.g., $\rightarrow$, and $\top$), as well as the dual modalities (e.g., $[ A ] \varphi \equiv \lnot \langle A \rangle \lnot \varphi$), can be derived in the standard way. Well-formed $\mathrm{HS_3}$-formulae can be obtained by the above grammar when $X \in \{ L, I \}$, while $\mathrm{HS_7}$-formulae are defined under the restriction that $X \in \{ L, AO, DBE \}$.

Fig. 1.

Allen’s interval relations, the corresponding $\mathrm{HS}$ modalities, and the semantic definitions $\mathrm{HS_3}$/$\mathrm{HS_7}$ modalities.

The semantics of ($\mathrm{HS}$ and) both $\mathrm{HS_3}$ and $\mathrm{HS_7}$ is given in terms of interval models $M = \langle \mathbb {I(D)},V\rangle$, where $\mathbb D$ is a linear order, $\mathbb {I(D)}$ is the set of all (strict) intervals over $\mathbb {D}$, and V is a valuation function $V : \mathcal {AP} \mapsto 2^{\mathbb {I(D)}}$, which assigns to each atomic proposition $p \in \mathcal {AP}$ the set of intervals V(p) on which p holds. The truth of a formula on a given interval [x, y] in an interval model M is defined by structural induction on formulae; propositional letters and Boolean connectives are treated in the standard way, while the semantic rules for the modal operators can be immediately deduced from Fig. 1. Formulae of $\mathrm{HS}$, and therefore of $\mathrm{HS_3}$ and $\mathrm{HS_7}$, can be interpreted over a class of interval models (built on a given class of linear orders). Among others, we mention the following classes of (interval models built on important classes of) linear orders: (i) the class of all linear orders $\mathsf {Lin}$; (ii) the class of (all) dense linear orders $\mathsf {Den}$, that is, those in which for every pair of distinct points there exists at least one point in between them (e.g., $\mathbb Q$ and $\mathbb R$); (iii) the class of (all) discrete linear orders $\mathsf {Dis}$, that is, those in which for every pair of distinct points there are only finitely many points in between them; (iv) the class of (all) finite linear orders $\mathsf {Fin}$, that is, those having only finitely many points; (v) the classes built on standard sets such as $\mathbb N,\mathbb Z,\mathbb Q$, etc. Given a class $\mathcal C$, and given $\mathbb D\in \mathcal C$, one can alternatively think of a $\mathrm{HS}$-model as a compass structure $\mathcal {G}=(\mathbb {D},\mathcal {L})$, where intervals [x, y] are seen as points (x, y) in the half-plane $\mathbb D\times \mathbb D$ identified by the constraint $x<y$; in this view, one may think of $\mathcal {L}$ as an extended labeling $\mathcal {L}:\mathbb {D}\times \mathbb {D}\rightarrow 2^{Cl(\varphi )}$, where $Cl(\varphi )$ is the set of all sub-formulae of a given formula $\varphi$, and $\mathcal {L}(x,y)$ denotes the subset of $Cl(\varphi )$ of precisely those formulae that are true at the interval [x, y] (including propositional letters). Modal operators are then immediately interpreted in a geometric way (e.g., the modality $\langle B \rangle ,\langle \overline{B} \rangle$ correspond to moving on a vertical line in the plane, while $\langle E \rangle ,\langle \overline{E} \rangle$ correspond to moving on a horizontal line). Such an interpretation (see, e.g. [19]) works nicely also for fragments of $\mathrm{HS}$ such as $\mathrm{HS_3}$ and $\mathrm{HS_7}$; we will alternately use compass structures and interval models in the rest of the paper.

In this paper we focus on the decidability of the satisfiability problem for both $\mathrm{HS_3}$ and $\mathrm{HS_7}$. The relative expressive power of $\mathrm{HS}$, $\mathrm{HS_3}$, and $\mathrm{HS_7}$ is unknown, but partial results seem to indicate that it holds $\mathrm{HS_3} \prec \mathrm{HS_7} \prec \mathrm{HS}$ ($\prec$ is read as is strictly less expressive than). As a matter of fact, we can easily prove that $\mathrm{HS_3} \prec \mathrm{HS}$ in the finite case: a simple counterexample based on bisimulation (cfr. [13]) proves that, for example, $\langle B \rangle$ cannot be expressed in $\mathrm{HS_3}$. Recent results [9, 18] for the $\mathsf {AB\overline{BA}}$ fragment of $\mathrm{HS}$ gives us a partial result concerning the satisfiability problem for $\mathrm{HS_3}$: it turns out that $\mathrm{HS_3}$ $\prec \mathsf {AB\overline{BA}}$ (the modal operators $\langle L \rangle$ and $\langle \overline{L} \rangle$ are immediately expressed in terms of $\langle A \rangle$ and $\langle \overline{A} \rangle$, while the operator $\langle I\rangle$ can be obtained by means of a combination of the modalities in $\mathsf {AB\overline{BA}}$). Since $\mathsf {AB\overline{BA}}$ is decidable, but not primitive recursive, in the finite case [18] as well as in the cases of $\mathsf {Den},\mathbb Q$ [9], so is $\mathrm{HS_3}$. Here we prove that its satisfiability problem is in fact PSpace-complete (a much stronger result) in the finite case and PSpace-hard in all other classes. Similarly, we know that the $\mathrm{HS_7}$-modality $\langle DBE\rangle$ is enough to obtain undecidability in the finite/discrete case, as well as the cases of $\mathbb N$ and $\mathbb Z$ [17]; based on existing results, though, the status of $\mathrm{HS_7}$ interpreted in $\mathsf {Lin},\mathbb Q$ or $\mathsf {Den}$ is unknown. We prove here that, not surprisingly, it is undecidable when interpreted on each of the mentioned classes of linearly ordered sets; our proof also applies to all cases already covered from [17].

3 Decidability and Hardness Results for $\mathrm{HS_3}$

In this section, we first prove that the satisfiability problem for $\mathrm{HS_3}$ is PSpace-hard, regardless of the class of linearly ordered sets on which it is interpreted. PSpace-hardness is proven via a (logspace) reduction from the classical Quantified Boolean Formula (QBF) satisfiability problem, shown to be PSpace-hard in [23]. A Quantified Boolean formula is an expression of the form $\theta \equiv Q_1 p_1 \ldots Q_n p_n f,$ where f is a formula of propositional logic and, for all $1\le i\le n$, $Q_i$ is either $\forall$ or $\exists$. We can assume without loss of generality that the formula $\theta$ is closed (i.e., every variable in f is quantified).

Theorem 1

The satisfiability problem for $\mathrm{HS_3}$ over $\mathsf {Fin},\mathsf {Dis},\mathsf {Den},\mathbb N,$ $\mathbb Z,\mathbb Q,$ and $\mathsf {Lin}$ is PSpace-hard.

Proof

(Sketch). Let $\theta = Q_1 p_1 \ldots Q_n$ $p_n f$ be a given closed Quantified Boolean formula. We build a $\mathrm{HS_3}$-formula $\varPhi _\theta$ such that $\varPhi _\theta$ is satisfiable over a linear order if and only if $\theta$ is true. Given $\theta$, we define $P_\forall = \{i: 1\le i \le n, Q_i=\forall \}$; the formula $\varPhi _\theta$, that uses an universal operator defined as $[ G ] \phi \equiv [I][I]\phi$, is the conjunction of the following formulae:

$$ \begin{array}{lll} \phi _1&{}\equiv &{}[ G ] (\mathop {\bigwedge }\nolimits _{1\le i \le n+1} ( h_i \rightarrow \mathop {\bigwedge }\nolimits _{1\le i \le n+1} [I]\lnot h_i )) \wedge [ G ] (\mathop {\bigwedge }\nolimits _{1\le i \le n} (h_i \rightarrow \langle I\rangle \langle I\rangle h_{i+1}))\\ \phi _2&{}\equiv &{}\langle I\rangle h_1\wedge [ G ] f \wedge [ G ] \mathop {\bigwedge }\nolimits _{i\in P_\forall } (h_i \rightarrow (\langle I\rangle \langle I\rangle (h_{i+1}\wedge p_i) \wedge \langle I\rangle \langle I\rangle (h_{i+1}\wedge \lnot p_i)))\\ \phi _3 &{}\equiv &{}[ G ] \mathop {\bigwedge }\nolimits _{2\le i\le n} ((h_i \wedge p_{i-1}) \rightarrow \\ &{} &{} [I]\mathop {\bigwedge }\nolimits _{1\le j \le i-1} ([I]\lnot h_{j} \rightarrow [I](\mathop {\bigvee }\nolimits _{i+1\le j \le n+1} h_j \rightarrow p_{i-1} ))) \\ \phi _4 &{}\equiv &{}[ G ] \mathop {\bigwedge }\nolimits _{2\le i\le n} ((h_i \wedge \lnot p_{i-1}) \rightarrow \\ &{} &{} [I]\mathop {\bigwedge }\nolimits _{1\le j \le i-1} ([I]\lnot h_{j} \rightarrow [I](\mathop {\bigvee }\nolimits _{i+1\le j \le n+1} h_j \rightarrow \lnot p_{i-1} ))) \\ \end{array} $$

Each $h_i$ ($1\le i\le n$) represents the node in the ($\theta$-)tree in which we choose the value of the variable $p_i$ (see Fig. 2). Assuming that $\theta$ has at least one proposition, $\langle I\rangle h_1$ (in $\phi _2$) forces that $h_1$ holds somewhere, and, then, we force the existence of a choice for each proposition ($\phi _1$); intervals representing choices are not pairwise intersecting ($\phi _1$), giving rise to a tree-like structure. For each universally quantified variable, we have intervals, in the correct sub-tree, that witness both the false and the true value for it ($\phi _2$). Values are propagated in the correct sub-trees ($\phi _3,\phi _4$) in such a way that the interval labeled with $h_{n+1}$ is also labeled with the chosen truth values for each proposition, so to serve as a witness for the satisfiability of $\theta$: in particular, if some of the $h_{n+1}$-labeled intervals do not satisfy f, then $[ G ] f$ is not satisfied either. Notice that this particular result holds also for the fragment of $\mathrm{HS_3}$ with the sole operator $\langle I\rangle$.    $\square$

Fig. 2.

A tree-model for $\theta =\forall p_1 \exists p_2 \forall p_3 \exists p_4 (p_1 \vee p_2) \wedge (\lnot p_1 \vee \lnot p_2) \wedge (p_3 \vee p_4) \wedge (\lnot p_3\vee \lnot p_4)$ (right-hand side) and its embedding into a compass structure (left-hand side).

Now, we prove that the satisfiability problem for $\mathrm{HS_3}$ is decidable in PSpace in the particular case of finite linear orders, giving us a completeness result in this case. While transferring such a result to other discrete classes is a purely technical problem, for the non-discrete ones it might require a deeper analysis.

Theorem 2

The satisfiability problem for $\mathrm{HS_3}$ over $\mathsf {Fin}$ is PSpace-complete.

Proof

(Sketch). Let $\varphi$ be an $\mathrm{HS_3}$ formula, and $\mathcal {G}=(\mathbb {D},\mathcal {L})$ be a compass structure for it. We prove that if $|\mathbb {D}|$ is greater than a certain limit (that will be obtained below) then there exists a compass structure $\mathcal {G}' =( \mathbb {D}',\mathcal {L}' )$ for $\varphi$ with $|\mathbb {D}'|<|\mathbb {D}|$. The contraction method obtained in this way can be iterated in order to obtain a model whose cardinality is less than or equal to the given limit. Since one can design an algorithm that only keeps trace of a constant number of horizontal lines (later referred to as rows) of a structure at the same time, finite satisfiability can be checked in $\textsc {PSpace}$. The intuitive idea of the contraction procedure is as follows: (i) we describe a row of the compass structure in such a way that the number of different descriptions is bounded; (ii) whenever the cardinality of the model is grater that the limit, then there must be two different rows $y_1<y_2$ with the same description; (iii) a smaller (contracted) model can be obtained by keeping the part of the original model below row $y_1$, and suitably reconstructing the rest of the model using the part of the original model above row $y_2$, thus eliminating the portion of the model $y_1$ and $y_2$.

Given $\mathcal {G}=(\mathbb {D},\mathcal {L})$ that satisfies $\varphi$, for a point (x, y) we can define $\mathcal {R} eq_{I\overline{L}}(x,y)=\{\langle I\rangle \psi ,[I]\psi ,\langle \overline{L} \rangle \psi ,[ \overline{L} ] \psi \,\,|\,\,\langle I\rangle \psi ,[I]\psi ,\langle \overline{L} \rangle \psi ,[ \overline{L} ] \psi \in \mathcal {L}(x,y)\}$; clearly, we have that $|\mathcal {R} eq_{I\overline{L}}(x,y)|\le |\varphi |$. Now, given an element $y\in \mathbb {D}$, let $\mathcal {R} eq_{I\overline{L}}(y)=\{ \mathcal {R} eq_{I\overline{L}}(x,y): 0\le x\le y \}$. Since $\langle I\rangle$ and $\langle \overline{L} \rangle$ are transitive, $|\mathcal {R} eq_{I\overline{L}}(y)|\le |\varphi |$ and its elements may be arranged in a sequence $R_1\subset \ldots \subset R_{|\mathcal {R} eq_{I\overline{L}}(y)|}$. The number of possible different chains $\mathcal {R} eq_{I\overline{L}}(y)$ is bounded by $|\varphi |^{|\varphi |}=2^{|\varphi |\log (|\varphi |)}$. Let $count_y: \mathcal {R} eq_{I\overline{L}}(y) \rightarrow \{1,\ldots , |\varphi |\}$ be a function such that for each $R\in \mathcal {R} eq_{I\overline{L}}(y)$ we have $count_y(R)= \min (2\cdot |\varphi | + 1, |\{x: \mathcal {R} eq_{I\overline{L}}(x,y)=R \}| )$. Observe that for any given $\mathcal {R} eq_{I\overline{L}}(y)$ we may have $(2\cdot |\varphi | +1)^{|\varphi |}=2^{|\varphi |\log (2\cdot |\varphi |+1)}$ possible $count_y$ functions. To each y we associate a minimal set $\mathcal {W}_y\subseteq \{0,\ldots ,y\}$ that satisfies: (i) for all $\psi \in Cl(\varphi )$ such that there exists $0\le x\le y$ and $y'>y$ with $\psi \in \mathcal {L}(x,y')$ there exists $x'\in \mathcal {W}_y$ and $y'>y$ such that $\psi \in \mathcal {L}(x',y')$, and (ii) for every $0\le x''\le y$ and $y''>y$ with $\psi \in \mathcal {L}(x'',y'')$, we have $y''\le y'$ or (iii) for every $0\le x''\le y$ and $y''>y$ with $\psi \in \mathcal {L}(x'',y'')$, we have $x''\ge x'$. Now, if $R_{\mathcal {W}_y}=\{ \psi : \exists x\exists y(0\le x\le y\wedge y'>y\wedge \psi \in \mathcal {L}(x,y'))\}$, we have that $| R_{\mathcal {W}_y}|\le {|\varphi |}$, and, thus, the number of possible $R_{\mathcal {W}_y}$ is bounded by $2^{2\cdot |\varphi |}$. Let $f_y:\mathcal {R} eq_{I\overline{L}}(y) \rightarrow \{0,\ldots , y\}$ such that, for every $R \in \mathcal {R} eq_{I\overline{L}}(y)$, $\mathcal {R} eq_{I\overline{L}}(f_y(R),y)=R$ and $\mathcal {R} eq_{I\overline{L}}(f_y(R)+1,y)\ne R$. Similarly to $\mathcal {R} eq_{I\overline{L}}(x,y)$, for every point (x, y) we can also define $\mathcal {R} eq_{L}(x,y)= \{\langle L \rangle \psi ,[ L ] \psi \,\,|\,\,\langle L \rangle \psi ,[ L ] \psi \in \mathcal {L}(x,y)\}$. Let us observe that for every $0\le x,x'\le y$, we have $\mathcal {R} eq_{L}(x,y)= \mathcal {R} eq_{L}(x',y)$ and thus we can simply identify with $\mathcal {R} eq_{L}(y)=\mathcal {R} eq_{L}(x,y)$ for some $0\le x\le y$. It is easy to see that $|\mathcal {R} eq_{L}(y)|\le |\varphi |$. Notice that $\mathcal {R} eq_{L}(y)$ is a set of sub-formulae of $\varphi$, while $\mathcal {R} eq_{I\overline{L}}(y)$ is a set of sets of sub-formulae of $\varphi$ whose cardinality cannot exceed $|\varphi |$. At this point, for each y we let $row(y)=( \mathcal {R} eq_{L}(y), \mathcal {R} eq_{I\overline{L}}(y), count_y, R_{\mathcal {W}_y})$. Taking into account the number of different component of each row(y), we have that the possible values for row(y) is roughly bounded by

$$|\varphi | \cdot 2^{|\varphi |\log (|\varphi |)}\cdot 2^{|\varphi | \log (2|\varphi |+1)}\cdot 2^{|\varphi |}=|\varphi |\cdot 2^{|\varphi | (\log (2|\varphi |+1) +\log (|\varphi |) + 1)}.$$

If $|\mathbb {D}|$ exceeds such a limit, then there must exist two rows $y_1<y_2$ with $row(y_1)=row(y_2)$. Thus, we can define a non-decreasing function $g:\{0,\ldots ,y_1 \}\rightarrow \{0,\ldots ,$ $y_2\}$ such that: (i) for every $x\in \{0,\ldots , y_1 \}$ we have $\mathcal {R} eq_{I\overline{L}}(x,y)=\mathcal {R} eq_{I\overline{L}}(x,g(x))$, and (ii) $\mathcal {W}_{y_2}\subseteq Img(g)$. Let $\varDelta =y_2-y_1$; we can finally build the compass structure $\mathcal {G}'=(\mathbb {D}', \mathcal {L}')$ with $|\mathbb {D}'|= |\mathbb {D}|-\varDelta$, where $\mathcal {L}'$ is defined as follows: (i) $\mathcal {L}'(x,y)=\mathcal {L}(x,y)$ for every $0\le x\le y\le y_1$, (ii) $\mathcal {L}'(x,y)= \mathcal {L}(x+\varDelta ,y+\varDelta )$ for every $y_1< x\le y\le |\mathbb {D}'|$, and (iii) $\mathcal {L}'(x,y)=\mathcal {L}(g(x),y+\varDelta )$ for every $y_1< x\le y_1 < y\le | \mathbb {D}'|$.

The above proof, usually called small model theorem, provides the necessary insights for developing a PSpace decision procedure for $\mathrm{HS_3}$ over $\mathsf {Fin}$. First observe that each formula $\varphi$ may be rewritten into an equi-satisfiable formula $\varphi '=\varphi \vee \langle I\rangle \varphi \vee \langle L \rangle \varphi$: it is easy to see there exists a compass structure $\mathcal {G}=(\mathbb {D},\mathcal {L})$ for $\varphi$ if and only if there exists a compass structure $\mathcal {G}' =(\mathbb {D},\mathcal {L}')$ for $\varphi '$ with $\varphi '\in \mathcal {L}(0,1)$. Then, we may assume w.l.o.g. that $\varphi =\varphi ' \vee \langle I\rangle \varphi ' \vee \langle L \rangle \varphi '$ for some formula $\varphi '$. A non-deterministic procedure can be designed that works as follows (where $\varphi$ is the formula to be checked for satisfiability):

• 1. A counter y is initialized to the value 0. Let F be an atom with $F \cap \{\langle I\rangle \psi \in Cl(\varphi )\}=\emptyset$ and $\varphi \in F$ - if such an atom does not exist we answer NO (unsatisfiable) - and let $row(y)=( \{\langle L \rangle \psi ,[ L ] \psi \in F \}, \{\{\langle I\rangle \psi ,[I]\psi ,\langle \overline{L} \rangle \psi ,[ \overline{L} ] \psi \in F \}\}, count_y, \{\psi : \langle I\rangle \psi \in F \})$ where $count_y(\{\langle I\rangle \psi ,[I]\psi ,\langle \overline{L} \rangle \psi ,[ \overline{L} ] \psi \in F \}) =~1$;

• 2. We generate a row $row(y+1)=( \mathcal {R} eq_{L}(y+1), \mathcal {R} eq_{I\overline{L}}(y+1), count_{y+1}, R_{\mathcal {W}_{y+1}})$ which is compatible with $row(y)=( \mathcal {R} eq_{L}(y), \mathcal {R} eq_{I\overline{L}}(y), count_y, R_{\mathcal {W}_y})$ - if such a row does not exist we answer NO, and if $\mathcal {R} eq_{L}(y+1)\cap \{ \langle L \rangle \psi \in Cl(\varphi ) \}=R_{\mathcal {W}_{y+1}}=\emptyset$ we answer YES;

• 3. If $y+1 = |\varphi |\cdot 2^{|\varphi | (\log (2|\varphi |+1) +\log (|\varphi |) + 1)} +1$ we answer NO, and, otherwise, we update y to $y+1$ and we go back to step 2.

It is easy to see that such a procedure may be implemented in polynomial space. As a matter of fact, the procedure requires to store only the counter for y and at most two rows at the same time; therefore, it suffices to prove that they can be represented in polynomial space w.r.t. $|\varphi |$. Since y cannot exceed $2^{|\varphi |(\log (2|\varphi |+1) +\log (|\varphi |) + 1)}$, we have that ${|\varphi | (\log (2|\varphi |+1) +\log (|\varphi |) + 1)}$ bits are enough to represent it. Since $|\mathcal {R} eq_{I\overline{L}}(y)|=|Dom(count_y)|\le |\varphi |$, we have that $count_y$ takes ${|\varphi |^2(\log (2|\varphi |+1) +\log (|\varphi |) + 1)}$ bits to be represented. Finally, we have that $|\mathcal {R} eq_{L}(F)|\le |\varphi |$, that $|\mathcal {R} eq_{I\overline{L}}(y)|\le |\varphi |$, that each element in $\mathcal {R} eq_{I\overline{L}}(y)$ requires $|\varphi |$ bits to be represented, and that $R_{\mathcal {W}_{y}}$ requires $2 \cdot |\varphi |$ bits to be represented. Summing up, we need $(\log (2|\varphi |+1) +\log (|\varphi |) + 1)(2|\varphi |+1) + 2 |\varphi |^2 + 4|\varphi |$ bits to handle the whole computation correctly, and thus the satisfiability of $\mathrm{HS_3}$ over $\mathsf {Fin}$ is in PSpace, as we claimed.    $\square$

4 Undecidability Results for $\mathrm{HS_7}$

In this section we show that the satisfiability problem for $\mathrm{HS_7}$ interpreted in any of the classes $\mathsf {Dis},\mathsf {Den},\mathbb N,\mathbb Z,\mathbb Q$, and $\mathsf {Lin}$ is undecidable (recall that $\mathsf {Dis}$, $\mathbb N$ and $\mathbb Z$ were already covered by the results in [17]). Undecidability is proven via a reduction [6] from the so-called Octant Tiling Problem (OTP). This is the problem of establishing whether a given finite set of tile types $\mathcal T=\{t_1,\ldots ,t_N\}$ can tile the second octant of the integer plane ${\mathcal O} = \{0 \le i \le j\}$. For every tile type $t_i \in {\mathcal T}$, let $right(t_i)$, $left(t_i)$, $up(t_i)$, and $down(t_i)$ be the colors of the corresponding sides of $t_i$. To solve the problem, one must find a function $f : {\mathcal O} \rightarrow {\mathcal T}$ such that ${right}(f(n,m)) = {left}(f(n+1,m))$ and ${up}(f(n,m)) = {down}(f(n,m+1))$. By exploiting an argument similar to the one used in [5] to prove the undecidability of the Quadrant Tiling Problem, it can be shown that the Octant Tiling Problem is undecidable too. Notice that the OTP, as well as our reduction, is unrelated to interpreting models as compass structures (as we did in the previous section).

Theorem 3

The satisfiability problem for $\mathrm{HS_7}$ over $\mathsf {Dis},\mathsf {Den},\mathbb N,\mathbb Z,\mathbb Q$, and $\mathsf {Lin}$ is undecidable.

Proof

(Sketch). Given an instance $\mathcal T$ of the OTP, where $\mathcal T$ is a finite set of tiles types, we build an $\mathrm{HS_7}$-formula $\varPhi _\mathcal T$ in such a way that $\varPhi _\mathcal T$ is satisfiable if and only if $\mathcal T$ tiles $\mathcal O$, assuming, here, that the underlying linear order presents at least one infinite ascending chain. We set the tiling framework by forcing the existence of an infinite chain of unit intervals (or, simply, units, denoted by the propositional letter u). Let us define an universal modality as $[ G ] \phi \equiv \phi \wedge \bigwedge _{X\in \{L,AO,DBE\}}([X]\phi \wedge [\overline{X}]\phi )$, a language $\mathbf L=\{*\} \cup \mathcal T,$ and let us identify each tile $t_1,\ldots ,t_N$ with a propositional letter whose symbol is used in the reduction. First, we have:

$$ \begin{array}{lll} \phi _1&{} \equiv &{} u_0\wedge \lnot *\wedge \mathop {\bigwedge }\nolimits _{l=0,1}[ G ] (u_l\rightarrow \langle AO \rangle u_{(l+1)~mod~2})\wedge [ G ] (u\leftrightarrow (u_0\vee u_1)) \\ \phi _2&{} \equiv &{} [ G ] (u\rightarrow (\langle DBE \rangle \top \wedge [ DBE ] \lnot u)) \wedge [ G ] ((u_0'\wedge u_1')\rightarrow \bot )\\ \phi _3&{} \equiv &{} \mathop {\bigwedge }\nolimits _{l=0,1}[ G ] (u_l\rightarrow [ DBE ] u_l')\\ \phi _4&{} \equiv &{} [ G ] (u\rightarrow [ DBE ] u')\wedge [ G ] ((u'\wedge [ AO ] \lnot u)\rightarrow u_b)\wedge [ G ] ((u'\wedge [ \overline{AO} ] \lnot u)\rightarrow u_e) \\ \phi _5&{} \equiv &{} [ G ] (u_b\rightarrow [ AO ] \lnot u)\wedge [ G ] (u_e\rightarrow [ \overline{AO} ] \lnot u) \end{array} $$

Assuming that $M,[x,y]\Vdash \phi _1\wedge \ldots \wedge \phi _5$ we can prove that there exists an infinite sequence $x<y=y_0<y_1<\ldots$ such that: (i) for each $i\ge 0$, $M,[y_i,y_{i+1}]\Vdash u$; (ii) if $[z,t]\ne [y_i,y_{i+1}]$, for each $i\ge 0$, then $M,[z,t]\Vdash \lnot u$, unless $t<x$ or $z>y_i$ for each $i\in \mathbb N$; (iii) for each $i\ge 0$, every interval of the type $[y_i,z]$, $z<y_{ i+1}$, satisfies $u_b$(and at least there exists one interval of this type), and every interval of the type $[z,y_{i+1}]$, $z>y_ i$, satisfies $u_e$ (and at least there exists one interval of this type). Now, consider the following formulae:

$$ \begin{array}{lll} \phi _6 &{}\equiv &{} C_1\wedge \mathop {\bigwedge }\nolimits _{l=0,1}[ G ] (C_l\rightarrow \langle AO \rangle C_{(l+1)~mod~2})\wedge [ G ] (C\leftrightarrow (C_0\vee C_1)) \\ \phi _7 &{}\equiv &{}\mathop {\bigwedge }\nolimits _{l=0,1}[ G ] (C_l\rightarrow [ DBE ] C_l') \wedge [ G ] ((C_0'\wedge C_1')\rightarrow \bot )\\ \phi _8 &{}\equiv &{} [ G ] (C\rightarrow ([ AO ] \lnot u_e\wedge [ \overline{AO} ] \lnot u_b)) \wedge [ G ] (C\rightarrow ([ DBE ] \lnot C \wedge \langle DBE \rangle \top )) \\ \phi _9 &{}\equiv &{}[ G ] (u \leftrightarrow \mathop {\bigvee }\nolimits _{s\in \mathbf L} s)\wedge [ G ] \mathop {\bigwedge }\nolimits _{s,s'\in \mathbf L,s\ne s'}(s\wedge s'\rightarrow \bot )\\ \phi _{10} &{}\equiv &{} \langle AO \rangle (\langle AO \rangle (\mathop {\bigvee }\nolimits _{i=1,\ldots ,N} t_i \wedge \langle AO \rangle *)) \wedge [ G ] ((u\wedge \langle AO \rangle C)\rightarrow \langle AO \rangle *)\\ \phi _{11} &{}\equiv &{} [ G ] ((u\wedge \langle \overline{AO} \rangle C)\rightarrow \langle \overline{AO} \rangle *) \wedge [ G ] (*\rightarrow (\langle AO \rangle C\vee \langle \overline{AO} \rangle C)\\ \phi _{12}&{}\equiv &{} [ G ] ((u\wedge \lnot *)\rightarrow \langle AO \rangle Corr)\wedge [ G ] ((u\wedge \lnot *\wedge [ AO ] \lnot *)\rightarrow \langle \overline{AO} \rangle Corr)\\ \phi _{13}&{}\equiv &{} [ G ] ((u\wedge \lnot *\wedge \langle AO \rangle *)\rightarrow [ AO ] (Corr\rightarrow \langle AO \rangle (u\wedge [ AO ] (u\rightarrow \lnot *))))\\ \phi _{14}&{}\equiv &{} [ G ] (Corr\rightarrow [ AO ] \lnot u_e)\wedge [ G ] (Corr\rightarrow [ \overline{AO} ] \lnot u_b) \wedge [ G ] (*\rightarrow [ AO ] \lnot Corr)\\ \phi _{15}&{}\equiv &{} [ G ] (Corr\rightarrow ([ DBE ] \lnot Corr\wedge [ DBE ] \lnot C\wedge [ \overline{DBE} ] \lnot C\wedge \lnot C)\\ \end{array} $$

Formulae from $\phi _6$ to $\phi _{15}$, in conjunction with the above observations, imply the existence of an infinite sequence of indexes $k_0<k_1<\ldots$ such that $y_0=y_{k_0}$ and: (i) for each $j\ge 0$, $M,[y_{k_j},y_{k_{j+1}}]\Vdash C$; if $[z,t]\ne [y_{k_j},y_{k_{j+1}}]$, for each $j\ge 0$, then $M,[z,t]\Vdash \lnot C$, unless $t<x$ or $z>y_i$ for each $i\in \mathbb N$. Moreover, these formulae guarantee that: (i) each u-interval of the type $[y_i,y_{i+1}]$ satisfies precisely one letter from $\mathbf L$; (ii) the C-interval $[y_{k_0},y_{k_{1}}]$ is composed by exactly three units; (iii) each C-interval of the type $[y_{k_j},y_{k_{j+1}}]$ is such that both its first unit $[y_{k_j},y_{{k_j}+1}]$ and its last unit $[y_{k_{j+1}-1},y_{k_{j+1}}]$ satisfies $*$; (iv) no other interval [z, t] satisfies $*$ unless $t<x$ or $z>y_i$ for each $i\in \mathbb N$. In the context of the structure above described, every level of the octant (C-interval) is composed by an integer number of units, the first one and the last one of which are the only $*$-intervals. We can therefore refer to the m-th $\lnot *$-interval of a level as the m-th tile of that level, and we are therefore interested in connecting the m-th tile of a given level with the m-th tile of the next one. This is taken care of by means of requirements from $\phi _{12}$ to $\phi _{14}$, which allow us to prove that: (i) for each $i,j\ge 0$, if the interval $[y_{{k_j}+i},y_{{k_j}+i+1}]$ is a $\lnot *$-interval, then the point $y_{k_j+i+1}$ starts a Corr-interval; (ii) for each $i,j>0$, if the interval $[y_{{k_j}+i+1},y_{{k_j}+i+2}]$ is a $\lnot *$-interval, then the point $y_{{k_j}+i}$ ends a Corr-interval; (iii) for each $j>0$ the points $y_{k_j},y_{{k_j}-1},$ and $y_{{k_j}-2}$ do not finish any Corr-interval; (iv) by a simple combinatorial argument, every tile of a level is connected (via Corr) to its corresponding tile of the next one, and, if the level is not the first one and the tile is not the last one of the level, the tile is also connected to the corresponding one of the preceding level; (v) finally, as a consequence of the above points, every level features precisely as many tiles as the preceding level plus one. To conclude, the following constraints:

$$ \begin{array}{lll} \phi _{16}&{}\equiv &{} \mathop {\bigwedge }\nolimits _{i=1,\ldots ,N} [ G ] (t_i \rightarrow [ AO ] (Corr\rightarrow \langle AO \rangle (\mathop {\bigvee }\nolimits _{j=1,\ldots ,N | up(t_i)=down(t_j)} t_j) ) )\\ \phi _{17}&{}\equiv &{} \mathop {\bigwedge }\nolimits _{i=1,\ldots ,N} [ G ] ( (t_i \wedge [ AO ] \lnot *)\rightarrow [ AO ] (\mathop {\bigvee }\nolimits _{j=1,\ldots ,N | right(t_i)=left(t_j)} t_j)) \end{array} $$

allow us to prove that: (i) for each pair $[y_i,y_{i+1}]$, $[y_{i+1},y_{i+2}]$ of $\lnot *$-intervals, if $[y_i,y_{i+1}]$ satisfies $t_r \in \mathcal T$ and $[y_{i+1},y_{i+2}]$ satisfies $t_s\in \mathcal T$ then $right(t_r)=left(t_s)$; (ii) for each interval $[y_i,y_j]$ satisfying Corr, if $[y_{i-1},y_i]$ satisfies $t_r \in \mathcal T$ and $[y_j,y_{j+1}]$ satisfies $t_s\in \mathcal T$ then $up(t_r)=down(t_s)$.    $\square$

Table 1. A summary of the results of this paper (denoted by [t.p.]).

5 Conclusions

In this paper we studied two previously unknown variants of Halpern and Shoham’s logic ($\mathrm{HS}$), inspired by Golumbic and Shamir’s interval algebras, which generalize the classical Allen’s Interval Algebra with coarser interval relations. While $\mathrm{HS_7}$ (the finest of them) is still generally undecidable, $\mathrm{HS_3}$ (the coarsest of them) becomes PSpace-complete in the finite case and, at least, PSpace-hard in the other cases (Table 1). Decidability in the infinite cases is still an open problem (via embedding we only know that it is decidable, but not primitive recursive - NPR, over $\mathsf {Den}$ and $\mathbb Q$), although our exploratory analysis of these cases suggests that $\mathrm{HS_3}$ should be PSpace-complete regardless of the class in which it is interpreted.