Temporal logic with recursion

We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments, thus obtaining 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 show 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.

Authors

• Florian Bruse
• Martin Lange

Keywords

• Temporal logic
• Recursion
• Fixpoint theory