Logo del repository
  1. Home
 
Opzioni

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

Bozzelli L.
•
Montanari A.
•
Peron A.
•
Sala P.
2024
  • journal article

Periodico
LOGICAL METHODS IN COMPUTER SCIENCE
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.
DOI
10.46298/lmcs-20(1:23)2024
WOS
WOS:001189929100001
Archivio
https://hdl.handle.net/11390/1274485
info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85188826834
https://ricerca.unityfvg.it/handle/11390/1274485
Diritti
open access
Soggetti
  • Complexity

  • Interval Temporal Log...

  • Satisfiability

  • Star-Free Regular Lan...

google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback