On the expressive power of CTL*

Rafal Somla

(Uppsala University)

In this talk, 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 second-order (set) quantification is restricted to paths. The result in itself is interesting and important for the problem of classifying temporal logics. However, of equal interest and importance is its method of proof, which exploits the use of Ehrenfeucht-Fraisse games.

(This is a presentation of the paper by Faron Moller and Alex Rabinovich from LICS'99. My purpose in studying it is to get a taste of "Games for Processes", which is the title of Faron's research project at Uppsala which I just started working on as a PhD student.)
Thursday 14th September 2000, 14:00
Robert Recorde Room
Department of Computer Science