Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculi

TL;DR

This paper demonstrates that the asynchronous pi-calculus cannot fully simulate the expressive power of the full pi-calculus due to its inability to break certain symmetries, establishing a fundamental separation in expressive capabilities.

Contribution

It proves the non-existence of a uniform, fully distributed translation from pi-calculus to asynchronous pi-calculus, highlighting limitations in expressive power.

Findings

Asynchronous pi-calculus cannot simulate full pi-calculus.

Symmetry-breaking limitations prevent full translation.

Separation results between pi-calculus, CCS, and internal mobility.

Abstract

The Asynchronous pi-calculus, proposed by Honda and Tokoro (1991) and, independently, by Boudol (1992), is a subset of the pi-calculus (Milner, 1992) which contains no explicit operators for choice and output-prefixing. The communication mechanism of this calculus, however, is powerful enough to simulate output-prefixing, as shown by Honda and Tokoro (1991) and by Boudol (1992), and input-guarded choice, as shown by Nestmann and Pierce (2000). A natural question arises, then, whether or not it is as expressive as the full pi-calculus. We show that this is not the case. More precisely, we show that there does not exist any uniform, fully distributed translation from the pi-calculus into the asynchronous pi-calculus, up to any "reasonable" notion of equivalence. This result is based on the incapability of the asynchronous pi-calculus to break certain symmetries possibly present in the initial communication graph. By similar arguments, we prove a separation result between the pi-calculus and CCS, and between the pi-calculus and the pi-calculus with internal mobility, a subset of the pi-calculus proposed by Sangiorgi where the output actions can only transmit private names.