Abstract of Paper

Why so many Temporal Logics Climb Up the Trees?
by A. Rabinovich and S. Maoz

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