|
Abstract : |
Relational Coarsest Partition Problems (RCPPs) play a vital role in verifying concurrent systems. It is known that RCPPs are P-complete and hence it may not be possible to design polylog time parallel algorithms for these problems. In this paper, we present a parallel algorithm for RCPP, in which its associated label transition system is assumed to have m transitions and n states. This algorithm runs in O(n1+)timeusing m n EREW PRAM processors, for any fixed <1. This algorithm is analogous and optimal with respect to the sequential algorithm of Kanellakis and Smolka. The same algorithm runs in time O(n log n) usingm log n log log n CRCW PRAM processors. We also describe implementation and experimental results on performance of our algorithm. 1, |
