2026-08-01T09:52:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5415 2024-03-06T10:36:24Z ddc:004 open_access

A Model Checking Procedure for Interval Temporal Logics based on Track Representatives Molinari, Alberto Montanari, Angelo Peron, Adriano Interval Temporal Logic Model Checking Complexity Model checking is commonly recognized as one of 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alberto Molinari and Angelo Montanari and Adriano Peron 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.193 urn:nbn:de:0030-drops-54150 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.193 eng https://creativecommons.org/licenses/by/3.0/legalcode