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

Authors: Faron Moller Alexander M. Rabinovich

Abstract

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.

BibTeX

  @InProceedings{MollerRabinovich-OntheExpressivePowe,
    author = 	 {Faron Moller and Alexander M. Rabinovich},
    title = 	 {On the Expressive Power of CTL},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {360--368},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }