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 BDAhomis EXPSPACE-COMPLETE.

The addition of temporal neighborhood makes the logic of prefixes and sub-intervals EXPSPACE-complete

Sala, P.
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 BDAhomis EXPSPACE-COMPLETE.
2024
Interval Temporal Logic
Star-Free Regular Languages
Satisfiability
Complexity
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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