# Understanding a Single Step in the Model Checking Algorithm

This answer explains roughly how to convert a nested boolean function into a Binary Decision Diagram (BDD). This question is about how to structure the states for the BDD. Now in this question I am trying to understand how to process the program states using a set of Binary Expressions I have (a specification), in Computation Tree Logic (CTL, a type of Temporal Logic).

Given that we have some "state BDDs", I am wondering the algorithm for processing the states, similar to what's described in (2) below. They mention representing both predicate transformers and fixpoints as BDD's. By predicate transformer, I'm guessing the tree format of the boolean equation, but not sure, and also not sure what the fixpoint is for.

As an example, they describe processing the CTL formula $\mathbf{EX}\alpha$.

$\mathbf{EX}\alpha$ means that there exists ($E$) a path starting from a state $s_0 \in S$ in which in the next ($X$) state $\alpha$ holds.

They mention:

The set $\{s \in S \mid \mathcal{M},s \vDash \varphi \}$ can be computed using basic BDDs operations plus fixpoint characterization of the CTL operators.

To summarize, wondering:

1. How to compute (at a high level) the set $\{s \in S \mid \mathcal{M},s \vDash \varphi \}$, using $\mathbf{EX}\alpha$ as an example. Perhaps using their example of $(a_1 \leftrightarrow a_2) \land (b_1 \leftrightarrow b_2)$ as the boolean expression for state (image below), or a different one, whatever's easier.
2. The basic data-structures and processes going on so I can figure out the details of an implementation.

(1) 2.1 Temporal Logic

A finite state system can be described as a tuple:

$$M =\langle S, I, R, L \rangle$$

where S is a finite set of states, $I \subseteq S$ is the set of initial states, and $R \subseteq S \times S$ is the transition relation, specifying the possible transitions from state to state. $L$ is a function that labels states with the atomic propositions from a given language. Such a tuple is called state transition graph or Kripke structure .

(2) 2.2 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 [below] depicts the BDD for the boolean formula $(a_1 \leftrightarrow a_2) \land (b_1 \leftrightarrow b_2)$, 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., $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.$^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 $\mathbf{EX}\alpha$. Let $\alpha(\bar{x})$ be a boolean formula on the boolean variables $\bar{x}$, where $\bar{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(\bar{x}) = \exists \bar{x}'.(\alpha(\bar{x})[\bar{x}'/\bar{x}] \land \mathcal{R}(\bar{x}, \bar{x}'))$$

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

The set $\{s \in S \mid \mathcal{M},s \vDash \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 \land \mathcal{I} = \bot$$ 