Abstract

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 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.

(Joint work with S. Maoz, Tel Aviv University)