CINECA IRIS Institutional Research Information System
IRIS è la piattaforma adottata dall’Università degli Studi di Udine per gestire l’archivio aperto dei prodotti della ricerca. L’archivio contiene articoli, contributi in volume, monografie, interventi pubblicati in atti di convegno, Tesi di dottorato e altri materiali.
EnglishThe 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.
| Titolo: | Interval temporal logic model checking: The border between good and bad HS fragments |
| Autori: | |
| Data di pubblicazione: | 2016 |
| 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. |
| Handle: | http://hdl.handle.net/11390/1089179 |
| ISBN: | 9783319402284 9783319402284 |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| ijcar.pdf | Documento in Pre-print | Non pubblico | Accesso ristretto Richiedi una copia |
http://hdl.handle.net/11390/1089179
Copyright © 2020