A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus

DOI10.1016/j.tcs.2011.02.034zbMath1216.68188OpenAlexW2123814533MaRDI QIDQ549180

Jan Friso Groote, Sjoerd Cranen, Michel Reniers

Publication date: 7 July 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.02.034

zbMATH Keywords

lineartranslationtemporal logicLTLCTL\(^*\)modal \(\mu \)-calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (4)

Unnamed Item ⋮ Unnamed Item ⋮ Justifications and a reconstruction of parity game solving algorithms ⋮ Loop-type sequent calculi for temporal logic

Uses Software

• mCRL2

Cites Work

• Programming languages and their definition. Selected papers ed. by C. B. Jones
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Model-checking processes with data
• Parameterised Boolean equation systems
• A lattice-theoretical fixpoint theorem and its applications
• Logic in Computer Science
• Theoretical Aspects of Computing – ICTAC 2005
• Instantiation for Parameterised Boolean Equation Systems
• Rudiments of \(\mu\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus