Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments

The model checking problem has thoroughly been explored in the context of standard point-based temporal logics, such as LTL, CTL, and CTL∗, whereas model checking for interval temporal logics has been brought to the attention only very recently. In this paper, we prove that the model checking problem for the logic of Allen’s relations started-by and finished-by is highly intractable, as it can be proved to be EXPSPACE-hard. Such a lower bound immedi- ately propagates to the full Halpern and Shoham’s modal logic of time intervals (HS). In contrast, we show that other noteworthy HS fragments, namely, Propositional Neighbourhood Logic extended with modalities for the Allen relation starts (resp., finishes) and its inverse started-by (resp., finished-by), turn out to have—maybe unexpectedly—the same complex- ity as LTL (i.e., they are PSPACE-complete), thus joining the group of other already studied, well-behaved albeit less expressive, HS fragments.