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 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.

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

Molinari, Alberto
;
2016-01-01

Abstract

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 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.
2016
978-3-319-40228-4
978-3-319-40229-1
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/316371
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact