CTL* and ECTL* as fragments of the modal mu-calculus
Mads DamAbstract: The modal mu-calculus of Kozen is a powerful logic for expressing temporal properties of programs. As a practical program specification tool, however, it suffers from not being very transparent. One problem is that the modal mu-calculus describe properties of states while most interesting temporal properties of programs are best described in terms of computation paths. With this in mind we present direct embeddings of the full branching time logics CTL* and its extended version ECTL* into the modal mu-calculus. The embeddings use tableaux as intermediate representations of formulas, and use extremal fixed points to characterise those paths through tableaux that are admissible in the sense that eventualities are guaranteed to be satisfied. The version of ECTL* considered here 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.
This report was published in Theoretical Computer Science 126 (1994) pp. 77-96.
Previous | Index | Next