## CTL* and ECTL* as fragments of the modal mu-calculus

**Mads Dam**
*Abstract:* 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.

*LFCS report ECS-LFCS-92-217*

This report was published in Theoretical Computer Science 126
(1994) pp. 77-96.

Previous |

Index |

Next