 Here we will briefly present the propositional modal interval logic proposed by Halpern and Shoham (1986), hereafter called \(\mathsf{HS}.\) The language of \(\mathsf{HS}\) includes a family of unary interval operators of the form \(\langle X\rangle,\) one for each of Allen’s interval relations over linear time. The respective notations are listed in Table 1  (Section 2.2). Given a set of atomic propositions \(PROP\), formulae are recusively defined by the following grammar:   \[\varphi := p \in {PROP} \mid \bot \mid \neg \varphi \mid (\varphi \wedge \varphi) \mid \langle X\rangle\varphi.\]