A THEORY OF BISIMULATION FOR THE PI-CALCULUS

We study a new formulation of bisimulation for the pi-calculus [MPW92] , which we have called open bisimulation (open bisimulation). In contr ast with the previously known bisimilarity equivalences, open biosimil ation is preserved by all pi-calculus operators, including input prefi x. The differences among all these equivalences already appear in the sublanguage without name restrictions: Here the definition of open bis imulation can be factorised into a ''standard'' part which, module the different syntax of actions, is the CCS bisimulation, and a part spec ific to the pi-calculus, which requires name instantiation. Attractive features of open biosimulation are: A simple axiomatisation (of the f inite terms), with a completeness proof which leads to the constructio n of minimal canonical representatives for the equivalence classes of open biosimulation; an ''efficient'' characterisation, based on a modi fied transition system. This characterisation seems promising for the development of automated-verification tools and also shows the call-by -need flavour of open biosimulationlar. Although in the paper we stick to the pi-calculus, the issues developed may be relevant to value-pas sing calculi in general.