The primary characteristic of interval temporal logic is that intervals, rather than points, are taken as the primitive ontological entities. Given their generally bad computational behavior of interval temporal logics, several techniques exist to produce decidable and computationally affordable temporal logics based on intervals. In this paper we take inspiration from Golumbic and Shamir's coarser interval algebras, which generalize the classical Allen's Interval Algebra, in order to define two previously unknown variants of Halpern and Shoham's logic (HS) based on coarser relations. We prove that, perhaps surprisingly, the satisfiability problem for the coarsest of the two variants, namely HS3, not only is decidable, but PSPACE-complete in the finite/discrete case, and PSPACE-hard in any other case; besides proving its complexity bounds, we implement a tableau-based satisfiability checker for it and test it against a systematically generated benchmark. Our results are strengthened by showing that not all coarser-than-Allen's relations are a guarantee of decidability, as we prove that the second variant, namely HS7, remains undecidable in all interesting cases.

On coarser interval temporal logics

Guido Sciavicco
Penultimo
;
STAN, IONEL EDUARD
Ultimo
2019

Abstract

The primary characteristic of interval temporal logic is that intervals, rather than points, are taken as the primitive ontological entities. Given their generally bad computational behavior of interval temporal logics, several techniques exist to produce decidable and computationally affordable temporal logics based on intervals. In this paper we take inspiration from Golumbic and Shamir's coarser interval algebras, which generalize the classical Allen's Interval Algebra, in order to define two previously unknown variants of Halpern and Shoham's logic (HS) based on coarser relations. We prove that, perhaps surprisingly, the satisfiability problem for the coarsest of the two variants, namely HS3, not only is decidable, but PSPACE-complete in the finite/discrete case, and PSPACE-hard in any other case; besides proving its complexity bounds, we implement a tableau-based satisfiability checker for it and test it against a systematically generated benchmark. Our results are strengthened by showing that not all coarser-than-Allen's relations are a guarantee of decidability, as we prove that the second variant, namely HS7, remains undecidable in all interesting cases.
2019
Emilio, Muñoz-Velasco; Mercedes, Pelegrín; Pietro, Sala; Sciavicco, Guido; Stan, IONEL EDUARD
File in questo prodotto:
File Dimensione Formato  
ai2018-LAST.pdf

accesso aperto

Descrizione: articolo
Tipologia: Pre-print
Licenza: Creative commons
Dimensione 571.5 kB
Formato Adobe PDF
571.5 kB Adobe PDF Visualizza/Apri
2019.on coarser interval temporal logics.pdf

solo gestori archivio

Tipologia: Full text (versione editoriale)
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 977.32 kB
Formato Adobe PDF
977.32 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in SFERA 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/11392/2398449
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 7
social impact