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.11
URN: urn:nbn:de:0030-drops-172585
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17258/
Go to the corresponding LIPIcs Volume Portal

Bozzelli, Laura ; Peron, Adriano

A Quantitative Extension of Interval Temporal Logic over Infinite Words

pdf-format:
LIPIcs-TIME-2022-11.pdf (0.8 MB)

Abstract

Model checking (MC) for Halpern and Shoham’s interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics), all of them assuming homogeneity in the propositional valuation. Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure. We introduce a quantitative extension of HS over traces, called Difference HS (DHS), allowing one to express timing constraints on the difference among interval lengths (durations). We show that MC and satisfiability of full DHS are in general undecidable, so, we investigate the decidability border for these problems by considering natural syntactical fragments of DHS. In particular, we identify a maximal decidable fragment DHS_{simple} of DHS proving in addition that the considered problems for this fragment are at least 2Expspace-hard. Moreover, by exploiting new results on linear-time hybrid logics, we show that for an equally expressive fragment of DHS_{simple}, the problems are Expspace-complete. Finally, we provide a characterization of HS over traces by means of the one-variable fragment of a novel hybrid logic.

BibTeX - Entry

@InProceedings{bozzelli_et_al:LIPIcs.TIME.2022.11,
  author =	{Bozzelli, Laura and Peron, Adriano},
  title =	{{A Quantitative Extension of Interval Temporal Logic over Infinite Words}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{11:1--11:16},
  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/17258},
  URN =		{urn:nbn:de:0030-drops-172585},
  doi =		{10.4230/LIPIcs.TIME.2022.11},
  annote =	{Keywords: Interval temporal logic, Homogeneity Assumption, Quantitative Constraints, Model checking, Decision Procedures, Complexity issues, Linear-time Hybrid Logics}
}

Keywords: Interval temporal logic, Homogeneity Assumption, Quantitative Constraints, Model checking, Decision Procedures, Complexity issues, Linear-time Hybrid Logics
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