Partitioning of the model.

One of the most important operations in model checking is the relational product:

$$\exists \ensuremath{\underline{x}} . (S(\ensuremath{\underlin... ...e T(\ensuremath{\underline{x}} ,\ensuremath{\underline{x}} '))$$

which computes the set of states reachable from $S(\ensuremath{\underline{x}} )$ through the transition relation $T(\cdot,\cdot)$. This operation can be performed as a single step by most BDD packages. Although it works quite well in practice, this operation has worst case exponential complexity [47]. The transition relation is said to be monolithic, as it consists of a single BDD.

In many practical cases, building the BDD for $T(\cdot,\cdot)$ may not be feasible. In many cases, however, it is possible to exploit the structure of the system and build the transition relation as a list of small BDDs, called clusters, which are implicitly disjoined (e.g., with an asynchronous model of concurrency) or conjoined (e.g., with synchronous systems) [9,10,11].

$$T(\cdot,\cdot) = \bigvee_i T_i(\cdot,\cdot)$$	disjunctive
$$T(\cdot,\cdot) = \bigwedge_i T_i(\cdot,\cdot)$$	conjunctive

In both cases the monolithic relational product is reduced to a sequence of disjunctively/conjunctively composed relational products on the clusters.

With a disjunctively partitioned transition relation, the relational product can be computed as follows:

$$\begin{array}{c}\displaystyle \exists \ensuremath{\underline... ...\underline{x}} ,\ensuremath{\underline{x}} ')) \\ \end{array}$$

In this way the relational product can be computed without ever building the BDD for the monolithic transition relation by distributing the existential quantification over disjunctions. The relational product is decomposed into a series of relational products involving relatively small BDDs.

For synchronous systems, NUSMV implements techniques based on early variable quantifications [59,9,10]. The basic idea is to find an ordering of the partitions $T_i(\cdot,\cdot)$ such that the quantification can be pushed inside the formula as much as possible, thus allowing relational products between small BDDs and existential quantification on a small number of variables, and thus reducing the complexity of the whole operation:

$$\begin{array}{l} \exists \ensuremath{\underline{x}} . (S(\en... ...\underline{x}} ,\ensuremath{\underline{x}} ')))\\ \end{array}$$

where $\ensuremath{\underline{x}} _i$ are disjoint sets of variables, $\ensuremath{\underline{x}} _i$ being the set of variables the $T_j(\cdot,\cdot)$ with j>i depends on, but $T_i(\cdot,\cdot)$ does not depend on.

NUSMV allows the user to perform model checking using the monolithic transition relation or the disjunctively or conjunctively partitioned transition relation. For conjunctive partitioning, the heuristics described in [35] and in [53] are available. They allow the user to compute the clusters for the conjunctively partitioned transition relation.