Next: Fields of Application Up: Symbolic Model Checking Previous: Temporal Logic

## Symbolic Representation of Kripke Structures

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 a1, a2, b1, b2. 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:

Where with we mean the simultaneous substitution in of variables with the corresponding variables . This operation, called Relational Product [47], is performed as an atomic operation on BDDs.

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:

NuSMV <>