An Infinite Hierarchy of Temporal Logics over Branching Time

Alexander Rabinovich

(University of Edinburgh)

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 and objective quantified `yardstick' to measure these logics.

We show that CTL^* has no finite base. 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; almost all these logics are inside the second level of our hierarchy.

We design new Ehrenfeucht-Fraisse games on trees, and use them as our main tool to prove inexpressibility.

(Based on joint work with Shahar Maoz)
Tuesday 17th October 2000, 14:00
Robert Recorde Room
Department of Computer Science