Comparing the expressive power of the synchronous and the asynchronous π-calculus

Abstract

The Asynchronous π-calculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the π-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 π-calculus. We show that this is not possible, i.e. there does not exist any uniform, parallel-preserving, translation from the π-calculus into the asynchronous π-calculus, up to any 'reasonable' notion of equivalence. This result is based on the incapability of the asynchronous π-calculus of breaking certain symmetries possibly present in the initial communication graph. By similar arguments, we prove a separation result between the π-calculus and CCS.