Temporal Logic over Branching Time: Expressiveness and Complexity.

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. In this talk we offer an explanation for the multiplicity of temporal logics over branching time and provide an objective quantified `yardstick' to measure these logics.