2/2016 - Model Checking the Logic of Allen’s Relations Meets and Started-by is PNP-Complete
Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala
| Titolo | Model Checking the Logic of Allen’s Relations Meets and Started-by is PNP-Complete |
|---|---|
| Numero | 2/2016 |
| Sottomesso da | Alberto Molinari |
| Sottomesso il | 17/7/2016 |
| Stato | Submitted |
| Autori | Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala |
| Abstract | 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). |
| File | 2-2016-Molinari.pdf |