In this paper, we prove PSPACE-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality (E), for the "suffix" relation on pairs of intervals, and modality (D), for the "sub-interval" relation, under the homogeneity assumption. The result significantly improves the EXPSPACE upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes ((E)) or, symmetrically, the modality for prefixes ((B)) to the logic of sub-intervals (featuring only (D)). & COPY; 2023 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).
Pspace-completeness of the temporal logic of sub-intervals and suffixes
Montanari, Angelo;Sala, Pietro
2023-01-01
Abstract
In this paper, we prove PSPACE-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality (E), for the "suffix" relation on pairs of intervals, and modality (D), for the "sub-interval" relation, under the homogeneity assumption. The result significantly improves the EXPSPACE upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes ((E)) or, symmetrically, the modality for prefixes ((B)) to the logic of sub-intervals (featuring only (D)). & COPY; 2023 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.