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.2018.23
URN: urn:nbn:de:0030-drops-97880
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9788/
Go to the corresponding LIPIcs Volume Portal

Walega, Przemyslaw Andrzej

Computational Complexity of a Core Fragment of Halpern-Shoham Logic

pdf-format:
LIPIcs-TIME-2018-23.pdf (0.5 MB)

Abstract

Halpern-Shoham logic (HS) is a highly expressive interval temporal logic but the satisfiability problem of its formulas is undecidable. The main goal in the research area is to introduce fragments of the logic which are of low computational complexity and of expressive power high enough for practical applications. Recently introduced syntactical restrictions imposed on formulas and semantical constraints put on models gave rise to tractable HS fragments for which prototypical real-world applications have already been proposed. One of such fragments is obtained by forbidding diamond modal operators and limiting formulas to the core form, i.e., the Horn form with at most one literal in the antecedent. The fragment was known to be NL-hard and in P but no tight results were known. In the paper we prove its P-completeness in the case where punctual intervals are allowed and the timeline is dense.
Importantly, the fragment is not referential, i.e., it does not allow us to express nominals (which label intervals) and satisfaction operators (which enables us to refer to intervals by their labels). We show that by adding nominals and satisfaction operators to the fragment we reach NP-completeness whenever the timeline is dense or the interpretation of modal operators is weakened (excluding the case when punctual intervals are disallowed and the timeline is discrete). Moreover, we prove that in the case of language containing nominals but not satisfaction operators, the fragment is still NP-complete over dense timelines.

BibTeX - Entry

@InProceedings{walega:LIPIcs:2018:9788,
  author =	{Przemyslaw Andrzej Walega},
  title =	{{Computational Complexity of a Core Fragment of Halpern-Shoham Logic}},
  booktitle =	{25th International Symposium on Temporal Representation  and Reasoning (TIME 2018)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-089-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{120},
  editor =	{Natasha Alechina and Kjetil N{\o}rv{\aa}g and Wojciech Penczek},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9788},
  URN =		{urn:nbn:de:0030-drops-97880},
  doi =		{10.4230/LIPIcs.TIME.2018.23},
  annote =	{Keywords: Temporal Logic, Interval Logic, Computational Complexity, Hybrid Logic}
}

Keywords: Temporal Logic, Interval Logic, Computational Complexity, Hybrid Logic
Collection: 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)
Issue Date: 2018
Date of publication: 08.10.2018

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