2/2017 - An in-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions
Laura Bozzelli, Alberto Molinari, Angelo Montanari and Adriano Peron
| Titolo | An in-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions |
|---|---|
| Numero | 2/2017 |
| Sottomesso da | Alberto Molinari |
| Sottomesso il | 30/1/2017 |
| Stato | Submitted |
| Autori | Laura Bozzelli, Alberto Molinari, Angelo Montanari and Adriano Peron |
| Abstract | In this paper, we systematically investigate the model checking problem for interval temporal logic (ITL), where interval labeling is defined by means of regular expressions. In the last years, ITL 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 by imposing suitable restrictions on interval labeling, by either defining it in terms of the labeling of interval endpoints or by constraining a proposition letter to hold over an interval if and only if it holds over each component state (homogeneity assumption). A possible way of overcoming these limitations has been recently outlined by Lomuscio and Michaliszyn, who proposed to exploit regular expressions to define the behavior of proposition letters over intervals in terms of the component states. They proved the decidability of ITL model checking with regular expressions for some very restricted fragments of Halpern and Shoham’s interval temporal logic (HS), extended with epistemic operators, giving some rough upper bounds to its computational complexity. In this paper, we first prove that model checking for full HS with regular expressions is decidable. Then, we show that the formulas of a large class of HS fragments, namely, all fragments featuring (a subset of) HS modalities for the Allen’s relations meets, met-by, starts, and started-by, can be model checked in polynomial working space (model checking for all these fragments turns out to be PSPACE-complete). |
| File | 2-2017-Molinari.pdf |