Model checking is commonly recognized as one of the most effective tools for 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 sufficiently long tracks of a Kripke structure by equivalent shorter ones.
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives / Molinari, Alberto; Montanari, Angelo; Peron, Adriano. - 41:(2015), pp. 193-210. (Intervento presentato al convegno EACSL Annual Conference on Computer Science Logic tenutosi a Berlin nel september 2015) [10.4230/LIPIcs.CSL.2015.193].
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives
PERON, ADRIANO
2015
Abstract
Model checking is commonly recognized as one of the most effective tools for 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 sufficiently long tracks of a Kripke structure by equivalent shorter ones.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.