On the asynchronous nature of the asynchronous π-calculus

We address the question of what kind of asynchronous communication is exactly modeled by the asynchronous π-calculus (π _a ). To this purpose we define a calculus where channels are represented explicitly as special buffer processes. The base language for is the (synchronous) π-calculus, except that ordinary processes communicate only via buffers. Then we compare this calculus with π _a . It turns out that there is a strong correspondence between π _a and in the case that buffers are bags: we can indeed encode each π _a process into a strongly asynchronous bisimilar process, and each process into a weakly asynchronous bisimilar π _a process. In case the buffers are queues or stacks, on the contrary, the correspondence does not hold. We show indeed that it is not possible to translate a stack or a queue into a weakly asynchronous bisimilar π _a process. Actually, for stacks we show an even stronger result, namely that they cannot be encoded into weakly (asynchronous) bisimilar processes in a π-calculus without mixed choice.