One of the most important operations in model checking is the relational product:
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 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].
With a disjunctively partitioned transition relation, the relational
product can be computed as follows:
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 BDDs and existential
quantification on a small number of variables, and thus reducing the
complexity of the whole operation:
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  and in  are available. They allow the user to compute the clusters for the conjunctively partitioned transition relation.