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

Bruse, Florian ; Lange, Martin ; Lozes, Etienne

The Tail-Recursive Fragment of Timed Recursive CTL

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

Abstract

Timed Recursive CTL (TRCTL) was recently proposed as a merger of two extensions of the well-known branching-time logic CTL: Timed CTL on one hand is interpreted over real-time systems like timed automata, and Recursive CTL (RecCTL) on the other hand obtains high expressiveness through the introduction of a recursion operator. Model checking for the resulting logic is known to be 2-EXPTIME-complete.
The aim of this paper is to investigate the possibility to obtain a fragment of lower complexity without losing too much expressive power. It is obtained by a syntactic property called "tail-recursiveness" that restricts the way that recursive formulas can be built. This restriction is known to decrease the complexity of model checking by half an exponential in the untimed setting. We show that this also works in the real-time world: model checking for the tail-recursive fragment of TRCTL is EXPSPACE-complete. The upper bound is obtained by a standard untiming construction via region graphs, and rests on the known complexity of tail-recursive fragments of higher-order modal logics. The lower bound is established by a reduction from a suitable tiling problem.

BibTeX - Entry

@InProceedings{bruse_et_al:LIPIcs.TIME.2022.5,
  author =	{Bruse, Florian and Lange, Martin and Lozes, Etienne},
  title =	{{The Tail-Recursive Fragment of Timed Recursive CTL}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{5:1--5: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/17252},
  URN =		{urn:nbn:de:0030-drops-172527},
  doi =		{10.4230/LIPIcs.TIME.2022.5},
  annote =	{Keywords: formal specification, temporal logic, real-time systems}
}

Keywords: formal specification, temporal logic, real-time systems
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