Fourteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1999)

Paper: On the Expressive Power of CTL (at LICS 1999)

Authors: Faron Moller Alexander Rabinovich


We show that the expressive power of the branching time logic CTL coincides with that of the class of bisimulation invariant properties expressible in so-called monadic path logic: monadic second order logic in which set quantification is restricted to paths. In order to prove this result, we first prove a new Composition Theorem for trees. This approach is adapted from the approach of Hafer and Thomas in their proof that CTL coincides with the whole of monadic path logic over the class of full binary trees.


    author = 	 {Faron Moller and Alexander Rabinovich},
    title = 	 {On the Expressive Power of CTL},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {360--369},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}