Many temporal logics were suggested as branching time specification formalisms during the last 20 years. These logics were compared against each other for their expressive power, model checking complexity and succinctness. Yet, unlike the case for linear time logics, no canonical temporal logic of branching time was agreed upon. We offer an explanation for the multiplicity of temporal logics over branching time and provide an objective quantified `yardstick' to measure these logics. We define an infinite hierarchy $BTL_k$ of temporal logics and prove its strictness. We examine the expressive power of commonly used branching time temporal logics. We show that $CTL^{*}$ has no finite base, and that almost all of its many sub-logics suggested in the literature are inside the second level of our hierarchy. We introduce new Ehrenfeucht-Fraiss\'e games on trees, and use them as our main tool to prove inexpressibility.

ASTEC seminar
April 19, 2000

Place: Information technology, Uppsala University
Room: 1549
Time: 13.15 - 14.00 (+ coffee and discussion)

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.