TitoloInterval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments
Numero1/2016
Sottomesso daAlberto Molinari
Sottomesso il5/4/2016
StatoDraft
AutoriLaura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala
AbstractThe 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 immediately 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 complexity as LTL (i.e., they are PSPACE-complete), thus joining the group of other already studied, well-behaved albeit less expressive, HS fragments.

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-40229-1_27
File1-2016-molinari.pdf