PARALLEL ALGORITHMS FOR RELATIONAL COARSEST PARTITION PROBLEMS

Relational Coarsest Partition Problems (RCPPs) play a vital role in ve rifying concurrent systems. It is known that RCPPs are P-complete and hence it may not be possible to design polylog time parallel algorithm s for these problems. In this paper, we present two efficient parallel algorithms for RCPP in which its associated label transition system i s assumed to have m transitions and n states. The first algorithm runs in O(n(1+epsilon)) time using m/n(epsilon) CREW PRAM processors, for any fixed epsilon < 1. This algorithm is analogous to and optimal with respect to the sequential algorithm of Kanellakis and Smolka. The sec ond algorithm runs in O(n log n) time using m/n CREW PRAM processors. This algorithm is analogous to and nearly optimal with respect to the sequential algorithm of Paige and Tarjan.