This Article 
 Bibliographic References 
 Add to: 
Parallel Algorithms for Relational Coarsest Partition Problems
July 1998 (vol. 9 no. 7)
pp. 687-699

Abstract—Relational Coarsest Partition Problems (RCPPs) play a vital role in verifying concurrent systems. It is known that RCPPs are ${\cal P}-{\rm complete}$ and hence it may not be possible to design polylog time parallel algorithms for these problems. In this paper, we present two efficient parallel algorithms for RCPP in which its associated label transition system is assumed to have m transitions and n states. The first algorithm runs in $O(n^{1+\epsilon})$ time using ${\textstyle{m \over {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 second algorithm runs in O(n log n) time using ${\textstyle{m \over n}}$ CREW PRAM processors. This algorithm is analogous to and nearly optimal with respect to the sequential algorithm of Paige and Tarjan.

[1] C. Alvarez, J.L. Balcazar, J. Gabarro, and M. Santha, Parallel Complexity in the Design and Analysis of Concurrent Systems. Springer-Verlag, 1991.
[2] H. Ben-Abdallah, D. Clarke, I. Lee, and O. Sokolsky, "PARAGON: A Paradigm for the Specification, Verification, and Testing of Real-Time Systems," Proc. IEEE Aerospace Conf., pp. 469-488, 1997.
[3] J. Bergstra and J. Klop, "Algebra of Communicating Processes with Abstraction," J. Theoretical Computer Science, vol. 37, pp. 77-121, 1985.
[4] P.C.P. Bhatt, K. Diks, T. Hagerup, V.C. Prasad, T. Radzik, and S. Saxena, "Improved Deterministic Parallel Integer Sorting," Information and Computation, pp. 29-47, 1991.
[5] R.P. Brent, "The Parallel Evaluation of General Arithmetic Expressions," J. ACM, vol. 21, pp. 201-206, 1974.
[6] E.M. Clarke and J.M. Wing, "Formal Methods: State of the Art and Future Directions," ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, 1996.
[7] R. Cleaveland, J.N. Gada, P.M. Lewis, S.A. Smolka, O.V. Sokolsky, and S. Zhang, "The Concurrency Factory—Practical Tools for Specification, Simulation, Verification, and Implementation of Concurrent Systems," Proc. DIMACS Workshop on Specification Techniques for Concurrent Systems,Princeton, N.J., 1994.
[8] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 36-72.
[9] R. Cleaveland and S.A. Smolka, "Strategic Directions in Concurrency Research," ACM Computing Surveys, vol. 28, no. 4, pp. 607-625, 1996.
[10] R. Cole, "Parallel Merge Sort," SIAM J. Computing, vol. 17, pp. 770-785, 1988.
[11] J.-C. Fernandez, "An Implementation of an Efficient Algorithm for Bisimulation Equivalence," Science of Computer Programming, vol. 13, pp. 219-236, 1989/90.
[12] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[13] J. J'aJ'a, An Introduction to Parallel Algorithms.New York: Addison-Wesley, 1992.
[14] P.C. Kanellakis and S.A. Smolka, "CCS Expressions, Finite State Processes, and Three Problems of Equivalence," Proc. Second Ann. ACM Symp. Principles of Distributed Computing, pp. 228-240, 1983.
[15] P.C. Kanellakis and S.A. Smolka, "CCS Expressions, Finite State Processes, and Three Problems of Equivalence," Information and Computation, pp. 43-68, vol. 86, 1990.
[16] R.E. Ladner and M.J. Fischer, "Parallel Prefix Computation," J. ACM, vol. 27, no. 4, pp. 831-838, Oct. 1980.
[17] F.T. Leighton,Introduction to Parallel Algorithms and Architectures: Arrays, Trees, Hypercubes.San Mateo, Calif.: Morgan Kaufmann, 1992.
[18] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[19] R. Paige and R.E. Tarjan, "Three Partition Refinement Algorithms," SIAM J. Computing, vol. 16, no. 6, pp. 973-989, 1987.
[20] S. Zhang and S.A. Smolka, "Towards Efficient Parallelization of Equivalence Checking Algorithms," Proc. FORTE '92—Fifth Int'l Conf. Formal Description Techniques, pp. 133-146, 1992.

Index Terms:
Bisimulation checking, coarsest partition problems, parallel algorithms, analysis of concurrent systems, labeled transition systems.
Sanguthevar Rajasekaran, Insup Lee, "Parallel Algorithms for Relational Coarsest Partition Problems," IEEE Transactions on Parallel and Distributed Systems, vol. 9, no. 7, pp. 687-699, July 1998, doi:10.1109/71.707548
Usage of this product signifies your acceptance of the Terms of Use.