Personal tools
You are here: Home Events Abstract Archives 2000 An infinite hierarchy of temporal logics over branching time

An infinite hierarchy of temporal logics over branching time

Alexander Rabinovich Tel Aviv University 4pm, Tuesday 31 October 2000 Room 3218, JCMB, King's Buildings

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)

Document Actions