On partitioning and symbolic model checking
Subramanian Iyer, Debashis Sahoo, E. Allen Emerson, Jawahar Jain · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2006
State-space-partitioning-based approaches have been proposed in the literature to address the state-explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of interpartition (crossover) image computations, which can be expensive. A model-checking algorithm that aggregates these expensive crossover images by localizing computation to individual partitions is presented. It reduces the number of crossover images and drastically outperforms extant approaches in terms of crossover image computation cost as well as total model-checking time, often by two orders of magnitude.