A partition refinement algorithm for the pi-calculus

The partition refinement algorithm is the basis for most of the tools for c hecking bisimulation equivalences and for computing minimal realisations of CCS-like finite state processes. In this paper, we present a partition ref inement algorithm for the n-calculus, a development of CCS where channel na mes can be communicated. It can be used to check bisimilarity and to comput e minimal realisations of finite control processes-the n-calculus counterpa rt of CCS finite state processes. The algorithm is developed for strong ope n bisimulation and can be adapted to late and early bisimulations, as well as to weak bisimulations. To arrive at the algorithm, a few laws, proof tec hniques, and four characterizations of open bisimulation are proved. (C) 20 01 Academic Press.