Comparing the expressive power of the Synchronous and the Asynchronous pi-calculus

TL;DR

This paper investigates whether the asynchronous pi-calculus can fully simulate the standard pi-calculus, concluding that it cannot due to limitations in breaking initial symmetries, thus highlighting fundamental expressive differences.

Contribution

It proves the impossibility of a uniform, parallel-preserving translation from pi-calculus to asynchronous pi-calculus, establishing a formal separation based on symmetry-breaking limitations.

Findings

No uniform translation exists from pi-calculus to asynchronous pi-calculus.

Asynchronous pi-calculus cannot break certain symmetries in initial communication graphs.

The paper also shows a separation between pi-calculus and CCS.

Abstract

The Asynchronous pi-calculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the pi-calculus 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 Boudol, and input-guarded choice, as shown recently by Nestmann and Pierce. A natural question arises, then, whether or not it is possible to embed in it the full pi-calculus. We show that this is not possible, i.e. there does not exist any uniform, parallel-preserving, translation from the pi-calculus into the asynchronous pi-calculus, up to any ``reasonable'' notion of equivalence. This result is based on the incapablity of the asynchronous pi-calculus of breaking certain symmetries possibly present in the initial communication graph. By similar arguments, we prove a separation result between the pi-calculus and CCS.