A linear translation from CTL^* to the first-order modal -calculus

DOI10.1016/J.TCS.2011.02.034zbMATH Open1216.68188OpenAlexW2123814533MaRDI QIDQ549180FDOQ549180

Authors: Sjoerd Cranen, Jan Friso Groote, Michel A. 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

Recommendations

• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• The modal \(\mu \)-calculus hierarchy over restricted classes of transition systems
• scientific article; zbMATH DE number 1456954
• General Models and Completeness of First-Order Modal  -calculus
• On guarded transformation in the modal \(\mu\)-calculus
• First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus
• scientific article; zbMATH DE number 2061706
• scientific article; zbMATH DE number 1341605
• On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
• On the expressivity of the modal mu-calculus

zbMATH Keywords

temporal logiclineartranslationLTLCTL\(^*\)modal \(\mu \)-calculus

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

• Loop-type sequent calculi for temporal logic
• Title not available (Why is that?)
• Modal logics for nominal transition systems
• Justifications and a reconstruction of parity game solving algorithms

Uses Software

• mCRL2

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q549180)