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.2020.6
URN: urn:nbn:de:0030-drops-129748
Go to the corresponding LIPIcs Volume Portal

Bruse, Florian ; Lange, Martin

Temporal Logic with Recursion

LIPIcs-TIME-2020-6.pdf (0.5 MB)


We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments. Unlike other proposals for modal fixpoint logics of high expressive power, we obtain logics that retain some of the appealing pragmatic advantages of CTL and LTL, yet have expressive power beyond that of the modal μ-calculus or MSO. We advocate these logics by showing how the recursion operator can be used to express interesting non-regular properties. We also study decidability and complexity issues of the standard decision problems.

BibTeX - Entry

  author =	{Florian Bruse and Martin Lange},
  title =	{{Temporal Logic with Recursion}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{6:1--6:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Emilio Mu{\~n}oz-Velasco and Ana Ozaki and Martin Theobald},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-129748},
  doi =		{10.4230/LIPIcs.TIME.2020.6},
  annote =	{Keywords: formal specification, temporal logic, expressive power}

Keywords: formal specification, temporal logic, expressive power
Collection: 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)
Issue Date: 2020
Date of publication: 15.09.2020

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