2026-07-23T21:24:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12974 2024-03-06T10:51:28Z ddc:004 open_access

Temporal Logic with Recursion Bruse, Florian Lange, Martin formal specification temporal logic expressive power 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Florian Bruse and Martin Lange 2020 Is Part Of LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2020.6 urn:nbn:de:0030-drops-129748 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.6 eng https://creativecommons.org/licenses/by/3.0/legalcode