3/2017 - On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions
Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron
| Titolo | On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions |
|---|---|
| Numero | 3/2017 |
| Sottomesso da | Alberto Molinari |
| Sottomesso il | 17/2/2017 |
| Stato | Submitted |
| Autori | Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron |
| Abstract | In this paper, we investigate the model checking problem for Halpern and Shoham's interval temporal logic HS. In the last years, interval temporal logic model checking has received an increasing attention as a viable alternative to the traditional (point-based) temporal logic model checking, which can be recovered as a special case. Most results have been obtained under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over each component state. Recently, Lomuscio and Michaliszyn proposed a way to relax such an assumption by exploiting regular expressions to define the behavior of proposition letters over intervals in terms of their component states. The exact complexity of model checking for HS with regular expressions has been established only for a class of small/medium HS fragments featuring (a subset of) HS modalities for Allen's relations meets, met-by, starts, and started-by. In this paper, we focus on two (syntactically) larger fragments of HS with regular expressions, namely AA'BB'E' and AA'EB'E', and prove that their model checking problem is AEXP-Pol-complete. Such results improve the upper bounds known for the same fragments under the homogeneity assumption, whose precise complexity remains an open problem. |
| File | 3-2017-Molinari.pdf |