The first model checking algorithms used an explicit representation of the Kripke structure as a labeled, directed graph [23,28,51].^{3} A major improvement was achieved with the use of symbolic representations [29,49,59,12,47], based on the use of Ordered Binary Decision Diagrams [7,8] (BDDs for short). BDDs are a representation for boolean formulas, which is canonical once an order on the variables has been established. Figure 3 depicts the BDD for the boolean formula , using the variable ordering a_{1}, a_{2}, b_{1}, b_{2}. Solid lines represent ``then'' arcs (the corresponding variable has to be considered positive), dashed lines represent ``else'' arcs (the corresponding variable has to be considered negative). Paths from the root to the node labeled with ``1'' represent the satisfying assignments of the represented boolean formula (e.g., ). Intuitively, a state of the system is symbolically represented by an assignment of boolean values to the set of state variables.^{4} A boolean formula (and thus its BDD) is a compact representation of the set of the states represented by the assignments which make the formula true. Similarly, the transition relation can be expressed as a boolean formula in two sets of variables, one relative to the current state and the other relative to the next state.
This makes it possible to represent predicate transformers and fixpoints as BDDs. The basic boolean operations are handled by means of standard algorithms for computing boolean connectives with BDDs [7,8], and fix-point algorithms can be easily implemented in terms of basic BDD operations [12,47].
The basic computation step in the previously described predicate transformers
is the computation of the states satisfying
.
Let
be a boolean formula on the boolean variables
,
where
is a vector of boolean state variables, representing the set of states
satisfying .
The set of states satisfying
can be
computed as:
The set
can be computed using basic BDDs operations plus fixpoint
characterization of the CTL operators. Formally, the check which determines
whether the model verifies a property
(see Equation 2)
reduces to the following check between BDDs: