Efficient partition of state space for parallel reachability analysis

Summary form only given. As the model-checking (which is based on reachability analysis) becomes increasingly used in the industry, there is a big need for efficient new methods to deal with the large real-size designs. This paper presents a novel method for improving the performance of reachability analysis using parallelization techniques. We propose a new method for partitioning the large state space modeling industrial designs with hundreds of millions of states and transitions. This method partitions the state space by performing a combination of abstraction-partition-refinement on its structure. The reachability analysis is distributed on processes located on the different network machines. Each one owns a partition and executes the reachability analysis on it. The algorithm for parallel reachability analysis is designed by a way reducing the communication overhead between the processes. The experimental results on large real designs show that this method improves the quality of partitions, the communication overhead and then the overall performance of the reachability analysis.