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.TIME.2019.18
URN: urn:nbn:de:0030-drops-113768
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11376/
Go to the corresponding LIPIcs Volume Portal

Bozzelli, Laura ; Montanari, Angelo ; Peron, Adriano

Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic

pdf-format:
LIPIcs-TIME-2019-18.pdf (0.7 MB)

Abstract

The model-checking (MC) problem of Halpern and Shoham Interval Temporal Logic (HS) has been recently investigated in some papers and is known to be decidable. An intriguing open question concerns the exact complexity of the problem for full HS: it is at least EXPSPACE-hard, while the only known upper bound is non-elementary and is obtained by exploiting an abstract representation of Kripke structure paths called descriptors. In this paper we generalize the approach by providing a uniform framework for model-checking full HS and meaningful (almost maximal) fragments, where a specialized type of descriptor is defined for each fragment. We then devise a general MC alternating algorithm parameterized by the type of descriptor which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze the time complexity of the algorithm and give, by non-trivial arguments, tight bounds on the length of certificates. For two types of descriptors, we obtain exponential upper and lower bounds which lead to an elementary MC algorithm for the related HS fragments. For the other types of descriptors, we provide non-elementary lower bounds. This last result addresses a question left open in some papers regarding the possibility of fixing an elementary upper bound on the size of the descriptors for full HS.

BibTeX - Entry

@InProceedings{bozzelli_et_al:LIPIcs:2019:11376,
  author =	{Laura Bozzelli and Angelo Montanari and Adriano Peron},
  title =	{{Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11376},
  URN =		{urn:nbn:de:0030-drops-113768},
  doi =		{10.4230/LIPIcs.TIME.2019.18},
  annote =	{Keywords: Interval temporal logic, Model checking, Complexity and succinctness issues}
}

Keywords: Interval temporal logic, Model checking, Complexity and succinctness issues
Collection: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Issue Date: 2019
Date of publication: 07.10.2019

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