Computing bisimulations for finite-control π-calculus

Symbolic bisimulation avoids the ifinite branching problem caused by instantiating input names with all names in the standard definition of bisimulation in pi-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 notion of bisimulation is introduced, in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names. It is shown that the new notion captures symbolic bisimulation in a precise sense. Based on the new definition an efficient algorithm, which instantiates input names "on-the-fly", is presented to check bisimulations for finite-control pi-calculus.