CTL-ASTERISK AND ECTL-ASTERISK AS FRAGMENTS OF THE MODAL MU-CALCULUS

Direct embeddings of the full branching-time CTL* and its extension ECTL* into the modal mu-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 Buchi 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.