CTL* and ECTL* as fragments of the modal μ-calculus

Citations of this article
Mendeley users who have this article in their library.


Direct embeddings of the full branching-time CTL* and its extension ECTL* into the modal μ-calculus are presented. The embeddings use tableaux as intermediate representations of formulas, and use extremal fixed points to characterise those paths through tableaux that satisfy an admissibility criterion, guaranteeing eventualities to be eventually satisfied. The version of ECTL* considered replaces the entire linear-time fragment of CTL* by Büchi automata on infinite strings. As a consequence the embedding of ECTL* turns out to be computable in linear time, while the embedding of CTL* is doubly exponential in the worst case. © 1994.




Dam, M. (1994). CTL* and ECTL* as fragments of the modal μ-calculus. Theoretical Computer Science, 126(1), 77–96. https://doi.org/10.1016/0304-3975(94)90269-0

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free