License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.193
URN: urn:nbn:de:0030-drops-54150
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5415/
Go to the corresponding LIPIcs Volume Portal

Molinari, Alberto ; Montanari, Angelo ; Peron, Adriano

A Model Checking Procedure for Interval Temporal Logics based on Track Representatives

pdf-format:
12.pdf (0.7 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{molinari_et_al:LIPIcs:2015:5415,
  author =	{Alberto Molinari and Angelo Montanari and Adriano Peron},
  title =	{{A Model Checking Procedure for Interval Temporal Logics based on Track Representatives}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{193--210},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5415},
  URN =		{urn:nbn:de:0030-drops-54150},
  doi =		{10.4230/LIPIcs.CSL.2015.193},
  annote =	{Keywords: Interval Temporal Logic, Model Checking, Complexity}
}

Keywords: Interval Temporal Logic, Model Checking, Complexity
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI