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

which computes the set of states reachable from through the transition relation . This operation can be performed as a single step by most

In many practical cases, building the `BDD` for
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
`BDD`s, called clusters, which are implicitly disjoined (e.g., with an
asynchronous model of concurrency) or conjoined (e.g., with synchronous
systems) [9,10,11].

disjunctive | |

conjunctive |

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

In this way the relational product can be computed without ever building the

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
such that the
quantification can be pushed inside the formula as much as possible,
thus allowing relational products between small `BDD`s and existential
quantification on a small number of variables, and thus reducing the
complexity of the whole operation:

where are disjoint sets of variables, being the set of variables the with

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.

NuSMV <>