Interval temporal logics (ITLs) are logics for reasoning about temporal statements expressed over intervals, i.e., periods of time. The most famous ITL studied so far is Halpern and Shoham's HS, which is the logic of the thirteen Allen's interval relations. Unfortunately, HS and most of its fragments have an undecidable satisfiability problem. This discouraged the research in this area until recently, when a number non-trivial decidable ITLs have been discovered. This paper is a contribution towards the complete classification of all different fragments of HS. We consider different combinations of the interval relations begins (B), after (A), later (L) and their inverses Ā, B̄ and L̄. We know from previous works that the combination ABB̄Ā is decidable only when finite domains are considered (and undecidable elsewhere), and that ABB̄ is decidable over the natural numbers. We extend these results by showing that decidability of ABB̄ can be further extended to capture the language ABB̄L̄, which lies in between ABB̄ and ABB̄Ā, and that turns out to be maximal w.r.t decidability over strongly discrete linear orders (e.g. finite orders, the naturals, the integers). We also prove that the proposed decision procedure is optimal with respect to the EXPSPACE complexity class.

Begin, after, and later: A maximal decidable interval temporal logic

SCIAVICCO, Guido
Ultimo
2010

Abstract

Interval temporal logics (ITLs) are logics for reasoning about temporal statements expressed over intervals, i.e., periods of time. The most famous ITL studied so far is Halpern and Shoham's HS, which is the logic of the thirteen Allen's interval relations. Unfortunately, HS and most of its fragments have an undecidable satisfiability problem. This discouraged the research in this area until recently, when a number non-trivial decidable ITLs have been discovered. This paper is a contribution towards the complete classification of all different fragments of HS. We consider different combinations of the interval relations begins (B), after (A), later (L) and their inverses Ā, B̄ and L̄. We know from previous works that the combination ABB̄Ā is decidable only when finite domains are considered (and undecidable elsewhere), and that ABB̄ is decidable over the natural numbers. We extend these results by showing that decidability of ABB̄ can be further extended to capture the language ABB̄L̄, which lies in between ABB̄ and ABB̄Ā, and that turns out to be maximal w.r.t decidability over strongly discrete linear orders (e.g. finite orders, the naturals, the integers). We also prove that the proposed decision procedure is optimal with respect to the EXPSPACE complexity class.
File in questo prodotto:
File Dimensione Formato  
draftGANDALF2010.pdf

solo gestori archivio

Descrizione: Articolo
Tipologia: Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 297.16 kB
Formato Adobe PDF
297.16 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
1006.1407v1.pdf

accesso aperto

Tipologia: Full text (versione editoriale)
Licenza: PUBBLICO - Pubblico con Copyright
Dimensione 220.88 kB
Formato Adobe PDF
220.88 kB Adobe PDF Visualizza/Apri

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