Some temporal properties of reactive systems, such as actions with duration and temporal aggregations, which are inherently interval-based, can not be properly expressed by the standard, point-based temporal logics LTL, CTL and CTL⁎, as they give a state-by-state account of system evolution. Conversely, interval temporal logics—which feature intervals, instead of points, as their primitive entities—naturally express them. We study the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS), interpreted on Kripke structures, under the homogeneity assumption. HS is the best known interval-based temporal logic, which has one modality for each of the 13 ordering relations between pairs of intervals (Allen's relations), apart from equality. We focus on MC for some HS fragments featuring modalities for (a subset of) Allen's relations meet, met-by, started-by, and finished-by, showing that it is in PNP. Additionally, we provide some complexity lower bounds to the problem.

Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy / Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 262:(2018), pp. 241-264. [10.1016/j.ic.2018.09.006]

Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy

Bozzelli, Laura
;
Montanari, Angelo
;
Peron, Adriano
;
2018

Abstract

Some temporal properties of reactive systems, such as actions with duration and temporal aggregations, which are inherently interval-based, can not be properly expressed by the standard, point-based temporal logics LTL, CTL and CTL⁎, as they give a state-by-state account of system evolution. Conversely, interval temporal logics—which feature intervals, instead of points, as their primitive entities—naturally express them. We study the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS), interpreted on Kripke structures, under the homogeneity assumption. HS is the best known interval-based temporal logic, which has one modality for each of the 13 ordering relations between pairs of intervals (Allen's relations), apart from equality. We focus on MC for some HS fragments featuring modalities for (a subset of) Allen's relations meet, met-by, started-by, and finished-by, showing that it is in PNP. Additionally, we provide some complexity lower bounds to the problem.
2018
Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy / Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 262:(2018), pp. 241-264. [10.1016/j.ic.2018.09.006]
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0890540118301263-main.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Accesso privato/ristretto
Dimensione 1.05 MB
Formato Adobe PDF
1.05 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11588/727590
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 8
social impact