Symbolic Representation of Kripke Structures

  

Figure 3: A BDD for the formula ``(a1 iff a2) and (b1 iff b2)''.

The first model checking algorithms used an explicit representation of the Kripke structure as a labeled, directed graph [23,28,51].³ 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 $(a_1 \leftrightarrow a_2) \wedge (b_1 \leftrightarrow b_2)$, using the variable ordering a₁, a₂, b₁, b₂. 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., $a_1 \leftarrow 1, a_2 \leftarrow 1, b_1 \leftarrow 0, b_2 \leftarrow 0$). Intuitively, a state of the system is symbolically represented by an assignment of boolean values to the set of state variables.⁴ 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 $\mathbf{EX} \alpha$. Let $\alpha(\ensuremath{\underline{x}} )$ be a boolean formula on the boolean variables $\ensuremath{\underline{x}}$, where $\ensuremath{\underline{x}}$ is a vector of boolean state variables, representing the set of states satisfying $\alpha$. The set of states satisfying $\mathbf{EX} \alpha$ can be computed as:

$$(\mathbf{EX} \alpha) (\ensuremath{\underline{x}} ) = \exists ... ...{R}(\ensuremath{\underline{x}} ,\ensuremath{\underline{x}} '))$$

Where with $\alpha(\ensuremath{\underline{x}} )[\ensuremath{\underline{x}} '/\ensuremath{\underline{x}} ]$ we mean the simultaneous substitution in $\alpha(\ensuremath{\underline{x}} )$ of variables $\ensuremath{\underline{x}}$ with the corresponding variables $\ensuremath{\underline{x}} '$. This operation, called Relational Product [47], is performed as an atomic operation on BDDs.

The set $\{s \in \mathcal{S}\; \vert\; \mathcal{M},s \models \varphi \}$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 $\varphi$ (see Equation 2) reduces to the following check between BDDs:

$$\neg \varphi \wedge \mathcal{I} = \bot$$