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.ICALP.2017.120
URN: urn:nbn:de:0030-drops-74703
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7470/
Go to the corresponding LIPIcs Volume Portal

Bozzelli, Laura ; Molinari, Alberto ; Montanari, Angelo ; Peron, Adriano ; Sala, Pietro

Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption

pdf-format:
LIPIcs-ICALP-2017-120.pdf (0.6 MB)

Abstract

In this paper, we investigate the finite satisfiability and model checking problems for the logic D of the sub-interval relation under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over all its points. First, we prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete; then, we show that its model checking problem, over finite Kripke structures, is PSPACE-complete as well.

BibTeX - Entry

@InProceedings{bozzelli_et_al:LIPIcs:2017:7470,
  author =	{Laura Bozzelli and Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala},
  title =	{{Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{120:1--120:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7470},
  URN =		{urn:nbn:de:0030-drops-74703},
  doi =		{10.4230/LIPIcs.ICALP.2017.120},
  annote =	{Keywords: Interval Temporal Logic, Satisfiability, Model Checking, Decidability, Computational Complexity}
}

Keywords: Interval Temporal Logic, Satisfiability, Model Checking, Decidability, Computational Complexity
Collection: 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Issue Date: 2017
Date of publication: 07.07.2017

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