License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2022.10
URN: urn:nbn:de:0030-drops-172578
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17257/
Go to the corresponding LIPIcs Volume Portal

Guelev, Dimitar P.

Gabbay Separation for the Duration Calculus

pdf-format:
LIPIcs-TIME-2022-10.pdf (0.7 MB)

Abstract

Gabbay’s separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In particular it enables a concise proof of Kamp’s seminal expressive completeness theorem for LTL. In 2000, Alexander Rabinovich established an expressive completeness result for a subset of the Duration Calculus (DC), a real-time interval temporal logic. DC is based on the chop binary modality, which restricts access to subintervals of the reference time interval, and is therefore regarded as introspective. The considered subset of DC is known as the ⌈P⌉-subset in the literature. Neighbourhood Logic (NL), a system closely related to {DC}, is based on the neighbourhood modalities, also written ⟨A⟩ and ⟨ ̄A⟩ in the notation stemming from Allen’s system of interval relations. These modalities are expanding as they allow writing future and past formulas to impose conditions outside the reference interval. This setting makes temporal separation relevant: is expressive power ultimately affected, if past constructs are not allowed in the scope of future ones, or vice versa? In this paper we establish an analogue of Gabbay’s separation theorem for the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities, and the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities and chop-based analogue of Kleene star. We show that the result applies if the weak chop inverses, a pair binary expanding modalities, are given the role of the neighbourhood modalities, by virtue of the inter-expressibility between them and the neighbourhood modalities in the presence of chop.

BibTeX - Entry

@InProceedings{guelev:LIPIcs.TIME.2022.10,
  author =	{Guelev, Dimitar P.},
  title =	{{Gabbay Separation for the Duration Calculus}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/17257},
  URN =		{urn:nbn:de:0030-drops-172578},
  doi =		{10.4230/LIPIcs.TIME.2022.10},
  annote =	{Keywords: Gabbay separation, Neighbourhood Logic, Duration Calculus, expanding modalities}
}

Keywords: Gabbay separation, Neighbourhood Logic, Duration Calculus, expanding modalities
Collection: 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)
Issue Date: 2022
Date of publication: 29.10.2022

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