Computing Bisimulations for Finite-Controlπ-Calculus

Symbolic bisimulation avoids the infinite branching problem causedby instantiating input names with all names in the standard definition of bisimulation in л-calculus. However, it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly. In this paper a new notionof bisimulation is introduced, in which the manipulation of maximally consistent conditions is replaced with a syst…