The dark side of interval temporal logic: marking the undecidability border (Q2251125)

The basic system in the focus of consideration of the present paper is a modal logic for reasoning about interval structures introduced by Halpern and Shoham and called \(\mathsf{HS}\). The authors solve various open problems in the characterization of \(\mathsf{HS}\) fragments with respect to decidability/undecidability. To this effect they study specific relevant fragments of \(\mathsf{HS}\): the logics \(\mathsf{O}\) and \(\overline {\mathsf O}\) of Allen's relation \textit{overlaps} and its inverse, and the logics \({\mathsf {AD}}\), \(\mathsf {A}\overline {\mathsf D}\), \(\overline {\mathsf A}\mathsf D\) and \(\overline{\mathsf {AD}}\) of Allen's relations \textit{meets} and \textit{during} and their inverses. The main results of this paper are summarized by the authors as follows: ``First, we showed undecidability of the satisfiability problem for \({\mathsf O}\) and \(\overline{\mathsf O}\) over all meaningful classes of linear orders, including the classes of all, discrete, dense, and finite linear orders. As a direct consequence of this result, we got undecidability of \({\mathsf B}\overline {\mathsf E}\) and \(\overline {\mathsf {BE}}\), whose decidability status over the class of finite linear orders was still unknown. Then, we proved undecidability of the satisfiability problem for \(\mathsf{AD}\), \({\mathsf A}\overline {\mathsf D}\), \(\overline {\mathsf A}\mathsf D\) and \(\overline{\mathsf{AD}}\) over all classes of linear orders containing at least a linear order with an infinite sequence of points. Since undecidability of \(\mathsf{ AD}\), \({\mathsf A}\overline {\mathsf D}\), \(\overline {\mathsf A}\mathsf D\) and \( \overline{\mathsf {AD}}\) over the class of finite linear orders was already known, we can conclude that also for these fragments undecidability spans all important classes of linear orders''. The proof of these results involves reduction of two different problems, depending on the considered class of linear orders: a reduction of the octan tiling problem (the infinite case) and finite tiling problem (the finite case).