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.

(Joint work with Alexander Rabinovich, Tel Aviv University, and published in the Proceedings of LICS'99.)