Towards efficient parallelization of equivalence checking algorithms

Equivalence checking is an important method for verifying concurrent transition systems. Two efficient sequential algorithms (Kanellakis-Smolka and Paige-Tarjan) have been used for this purpose for some time. Discussions in the literature on the parallelization of these algorithms, however, seem to be few or none. In this paper, we present a parallel version of the Kanellakis-Smolka algorithm and some empirical timing results on an Intel iPSC/860 32-processor multicomputer. Although the equivalence checking problem has been shown to be P-complete - meaning, intuitively, that there is probably something inherently sequential about the problem - we have obtained non-trivial speedups for the cycler-based scheduler benchmark of Milner. Timing results are also presented for randomly generated transition systems.