A classic result by Stockmeyer [Sto74] gives a non-elementary lower bound to the emptiness problem for generalized ∗-free regular expressions. This result is intimately connected to the satisfiability problem for the interval temporal logic of the chop modality under the homogeneity assumption [HMM83]. The chop modality can indeed be viewed as the inverse of the concatenation operator of regular languages, and such a correspondence enables reductions between the two problems. In this paper, we study the complexity of the satisfiability problem for suitable weakenings of the chop interval temporal logic, that can be equivalently viewed as fragments of Halpern and Shoham interval logic. We first introduce the logic BDhom featuring modalities B (for begins), corresponding to the prefix relation on pairs of intervals, and D (for during), corresponding to the infix relation, whose satisfiability problem, under the homogeneity assumption, has been recently shown to be PSpace-complete [BMPS21b]. The homogeneous models of BDhom naturally correspond to languages defined by restricted forms of generalized *-free regular expressions, that feature operators for union, complementation, and the inverses of the prefix and infix relations. Then, we study the extension of BDhom with the temporal neighborhood modality A, corresponding to the Allen relation Meets, and prove that such an addition increases both the expressiveness and the complexity of the logic. In particular, we show that the resulting logic BDAhom is ExpSpace-complete.

THE ADDITION OF TEMPORAL NEIGHBORHOOD MAKES THE LOGIC OF PREFIXES AND SUB-INTERVALS EXPSPACE-COMPLETE

Peron A.;
2024-01-01

Abstract

A classic result by Stockmeyer [Sto74] gives a non-elementary lower bound to the emptiness problem for generalized ∗-free regular expressions. This result is intimately connected to the satisfiability problem for the interval temporal logic of the chop modality under the homogeneity assumption [HMM83]. The chop modality can indeed be viewed as the inverse of the concatenation operator of regular languages, and such a correspondence enables reductions between the two problems. In this paper, we study the complexity of the satisfiability problem for suitable weakenings of the chop interval temporal logic, that can be equivalently viewed as fragments of Halpern and Shoham interval logic. We first introduce the logic BDhom featuring modalities B (for begins), corresponding to the prefix relation on pairs of intervals, and D (for during), corresponding to the infix relation, whose satisfiability problem, under the homogeneity assumption, has been recently shown to be PSpace-complete [BMPS21b]. The homogeneous models of BDhom naturally correspond to languages defined by restricted forms of generalized *-free regular expressions, that feature operators for union, complementation, and the inverses of the prefix and infix relations. Then, we study the extension of BDhom with the temporal neighborhood modality A, corresponding to the Allen relation Meets, and prove that such an addition increases both the expressiveness and the complexity of the logic. In particular, we show that the resulting logic BDAhom is ExpSpace-complete.
2024
22-mar-2024
Pubblicato
File in questo prodotto:
File Dimensione Formato  
2202.07881 (1).pdf

accesso aperto

Tipologia: Documento in Versione Editoriale
Licenza: Creative commons
Dimensione 820.85 kB
Formato Adobe PDF
820.85 kB 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/3072418
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact