In the previous two chapters we presented temporal logics for reasoning about local properties of interpreted transition systems (BML) and about global properties of linear time models, that is, single computations (LTL). Neither of these, however, is expressive enough to reason about global properties of all computations in the transition system. This is where branching-time temporal logics come into play. They combine the full repertoire of temporal operators of LTL, on one hand, with the ability to quantify over paths, and hence over computations, starting at the current state.

The temporal operators X and U of LTL navigate forwards along a particular run and express global properties about it. Thus, LTL is suited for reasoning about single computations in a transition system, but does not provide any syntactic means to look at alternative runs in the system. On the other hand, BML provides the means to look at all immediate successors of the current state, but not any further. So, the idea of the branching-time framework is to put temporal operators and path quantifiers together and enable global reasoning about all possible computations starting from a given state, and eventually about what happens in the entire transition system. In particular, the path quantification can be regarded as a generalisation of both existential and universal model checking in LTL, but it also enables much more, viz. any Boolean combination of both, as well as iterating these by nesting path quantifiers. In the simplest cases of interaction between path quantifiers and temporal operators, these are required to alternate strictly and that restriction generates the simplest natural branching-time logics TLR and CTL which we study here. Gradually extending the admissible patterns of combinations of temporal and Boolean operators over what patterns of path quantification is allowed produces a growing hierarchy of more expressive logics, eventually leading to the fully unrestricted language of the branching-time logic CTL*.

We present in this chapter the most popular species of branching-time logics and discuss and compare their expressiveness. Nevertheless, the proofs about expressiveness results are deferred to Chapter 10 that is exclusively dedicated to those questions.