2/2015 - A Model Checking Procedure for Interval Temporal Logics based on Track Representatives
Alberto Molinari, Angelo Montanari, Adriano Peron
| Titolo | A Model Checking Procedure for Interval Temporal Logics based on Track Representatives |
|---|---|
| Numero | 2/2015 |
| Sottomesso da | Angelo Montanari |
| Sottomesso il | 27/1/2015 |
| Stato | Draft |
| Autori | Alberto Molinari, Angelo Montanari, Adriano Peron |
| Abstract | Model checking is commonly recognised as the most effective tool in system verification. While it has been systematically investigated in the context of classical, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACE-hardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones. |
| File | 2-2015-montanari.pdf |