TitoloA Model Checking Procedure for Interval Temporal Logics based on Track Representatives
Sottomesso daAngelo Montanari
Sottomesso il27/1/2015
AutoriAlberto Molinari, Angelo Montanari, Adriano Peron
AbstractModel 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.