Model Checking the Logic of Allen's Relations Meets and Started-by is P^NP-Complete

Laura Bozzelli
(Technical University of Madrid (UPM), Spain)
Alberto Molinari
(University of Udine, Italy)
Angelo Montanari
(University of Udine, Italy)
Adriano Peron
(University of Napoli "Federico II", Italy)
Pietro Sala
(University of Verona, Italy)

In the plethora of fragments of Halpern and Shoham's modal logic of time intervals (HS), the logic AB of Allen's relations Meets and Started-by is at a central position. Statements that may be true at certain intervals, but at no sub-interval of them, such as accomplishments, as well as metric constraints about the length of intervals, that force, for instance, an interval to be at least (resp., at most, exactly) k points long, can be expressed in AB. Moreover, over the linear order of the natural numbers N, it subsumes the (point-based) logic LTL, as it can easily encode the next and until modalities. Finally, it is expressive enough to capture the ω-regular languages, that is, for each ω-regular expression R there exists an AB formula Φ such that the language defined by R coincides with the set of models of Φ over N. It has been shown that the satisfiability problem for AB over N is EXPSPACE-complete. Here we prove that, under the homogeneity assumption, its model checking problem is Δ^p_2 = P^NP-complete (for the sake of comparison, the model checking problem for full HS is EXPSPACE-hard, and the only known decision procedure is nonelementary). Moreover, we show that the modality for the Allen relation Met-by can be added to AB at no extra cost (AA'B is P^NP-complete as well).

In Domenico Cantone and Giorgio Delzanno: Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2016), Catania, Italy, 14-16 September 2016, Electronic Proceedings in Theoretical Computer Science 226, pp. 76–90.
Published: 13th September 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: