State space partitioning-based approaches have been proposed in the literature to address the
state-space explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of inter-partition (
cross-over) image computations, which can be expensive. We present a model checking algorithm that aggregates these expensive cross-over images by localizing computation to individual partitions. It reduces the number of cross-over images and drastically outperforms extant approaches in terms of
cross-over image computation cost as well as total model checking time, often by two orders of magnitude.
Keywords: Symbolic Model Checking, BDD, state partitioning, CTL.