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