The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper [10], Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) is highly undecidable over any reasonable class of linear orders. In order to recover decidability, one can restrict the set of temporal modalities and/or the class of models. In the following, we focus on the satisfiability problem for HS fragments under the homogeneity assumption, according to which any proposition letter holds over an interval if only if it holds at all its points. The problem for full HShom has been shown to be non-elementarily decidable [13], but its only known lower bound is EXPSPACE (in fact, EXPSPACE-hardness has been shown for the logic of prefixes and suffixes BEhom, which is a very small fragment of it [3]). The logic of prefixes and infixes BDhom has been recently shown to be PSPACE-complete [5]. In this paper, we prove that the addition of the Allen relation Meets to BDhom makes it EXPSPACE-complete.

Adding the relation meets to the temporal logic of prefixes and infixes makes It EXPSPACEL-complete / Bozzelli, L.; Montanari, A.; Sala, P.; Peron, A.. - In: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. - ISSN 2075-2180. - 346:(2021), pp. 179-194. (Intervento presentato al convegno 12th International Symposium on Games, Automata, Logics, and Formal Verification, G and ALF 2021 tenutosi a ita nel 2021) [10.4204/EPTCS.346.12].

Adding the relation meets to the temporal logic of prefixes and infixes makes It EXPSPACEL-complete

Bozzelli L.;Montanari A.;Peron A.
2021

Abstract

The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper [10], Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) is highly undecidable over any reasonable class of linear orders. In order to recover decidability, one can restrict the set of temporal modalities and/or the class of models. In the following, we focus on the satisfiability problem for HS fragments under the homogeneity assumption, according to which any proposition letter holds over an interval if only if it holds at all its points. The problem for full HShom has been shown to be non-elementarily decidable [13], but its only known lower bound is EXPSPACE (in fact, EXPSPACE-hardness has been shown for the logic of prefixes and suffixes BEhom, which is a very small fragment of it [3]). The logic of prefixes and infixes BDhom has been recently shown to be PSPACE-complete [5]. In this paper, we prove that the addition of the Allen relation Meets to BDhom makes it EXPSPACE-complete.
2021
Adding the relation meets to the temporal logic of prefixes and infixes makes It EXPSPACEL-complete / Bozzelli, L.; Montanari, A.; Sala, P.; Peron, A.. - In: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. - ISSN 2075-2180. - 346:(2021), pp. 179-194. (Intervento presentato al convegno 12th International Symposium on Games, Automata, Logics, and Formal Verification, G and ALF 2021 tenutosi a ita nel 2021) [10.4204/EPTCS.346.12].
File in questo prodotto:
File Dimensione Formato  
2109.08320v1.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Versione Editoriale (PDF)
Licenza: Dominio pubblico
Dimensione 235.81 kB
Formato Adobe PDF
235.81 kB Adobe PDF Visualizza/Apri

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