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
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12974/
Bruse, Florian ;
Lange, Martin
Temporal Logic with Recursion
Abstract
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
@InProceedings{bruse_et_al:LIPIcs:2020:12974,
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 = {https://drops.dagstuhl.de/opus/volltexte/2020/12974},
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 |
