Model checking (MC) for Halpern and Shoham's interval temporal logic HS has been recently shown to be decidable. An intriguing open question is its exact complexity for full HS: it is at least EXPSPACE-hard, and the only known upper bound, which exploits an abstract representation of Kripke structure paths (descriptor), is non-elementary. In this paper, we provide a uniform framework to MC for full HS and meaningful fragments of it, with a specific type of descriptor for each fragment. Then, we devise a general MC alternating algorithm, parameterized by the descriptor's type, which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze its complexity and give tight bounds on the length of certificates. For two types of descriptor, we obtain exponential upper and lower bounds; for the other ones, we provide non-elementary lower bounds.

Complexity analysis of a unifying algorithm for model checking interval temporal logic

Peron A.
2021-01-01

Abstract

Model checking (MC) for Halpern and Shoham's interval temporal logic HS has been recently shown to be decidable. An intriguing open question is its exact complexity for full HS: it is at least EXPSPACE-hard, and the only known upper bound, which exploits an abstract representation of Kripke structure paths (descriptor), is non-elementary. In this paper, we provide a uniform framework to MC for full HS and meaningful fragments of it, with a specific type of descriptor for each fragment. Then, we devise a general MC alternating algorithm, parameterized by the descriptor's type, which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze its complexity and give tight bounds on the length of certificates. For two types of descriptor, we obtain exponential upper and lower bounds; for the other ones, we provide non-elementary lower bounds.
2021
1-nov-2020
Pubblicato
https://www.sciencedirect.com/science/article/pii/S0890540120301280
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0890540120301280-main.pdf

Accesso chiuso

Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 689.31 kB
Formato Adobe PDF
689.31 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
1-s2.0-S0890540120301280-main-Post_print.pdf

Open Access dal 02/11/2022

Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Creative commons
Dimensione 1.21 MB
Formato Adobe PDF
1.21 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

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/11368/3032609
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact