ON BISIMULATIONS FOR THE ASYNCHRONOUS PI-CALCULUS

The asynchronous pi-calculus is a variant of the pi-calculus where mes sage emission is nonblocking. Honda and Tokoro have studied a semantic s for this calculus based on bisimulation. Their bisimulation relies o n a modified transition system where, at any moment, a process can per form any input action. In this paper we propose a new notion of bisimu lation for the asynchronous pi-calculus, defined on top of the standar d labelled transition system. We give several characterizations of thi s equivalence including one in terms of Honda and Tokoro's bisimulatio n, and one in terms of barbed equivalence. We show that this bisimulat ion is preserved by name substitutions, hence by input prefix. Finally , we give a complete axiomatization of the (strong) bisimulation for f inite terms. (C) 1998-Elsevier Science B.V. All rights reserved.