Parallel and Complete Model Checking with Linear Complexity
Xiaojuan Wu · Journal of Information and Computational Science · 2013
In this paper, we present Parallel and Complete model checking algorithm. This algorithm can parallel find out all counterexamples of small system with linear complexity only by main memory. If the checked system with a large scale, the algorithm employs disks to store the states and searches out all the counterexamples whose I/O complexity is linear at any situation. With parallel technology, the searching procedure is accelerated by multiply. At the same time, we employ hash function to speed up the comparison. Our algorithm parallel starts from accepting states of system to find out accepting cycles. If system does not exist any accepting cycles, our algorithm would be terminated, because it means there are no counterexamples in system. It can save a lot of time. In the complexity analysis part, we compare our algorithm to another parallel algorithms, it shows the outperforms of our algorithm.