On the Validity of Encodings of the Synchronous in the Asynchronous $\pi$-calculus

TL;DR

This paper rigorously verifies that well-known encodings of the synchronous $alculus into its asynchronous fragment meet Gorla's criteria, clarifying their validity and the expressive power relationship.

Contribution

It formally proves the validity of Boudol's and Honda & Tokoro's encodings within Gorla's framework, confirming their correctness and implications for expressiveness.

Findings

The encodings satisfy Gorla's validity criteria.

Asynchronous $alculus is as expressive as the synchronous version.

Clarifies the relationship between different encodings and expressiveness.

Abstract

Process calculi may be compared in their expressive power by means of encodings between them. A widely accepted definition of what constitutes a valid encoding for (dis)proving relative expressiveness results between process calculi was proposed by Gorla. Prior to this work, diverse encodability and separation results were generally obtained using distinct, and often incompatible, quality criteria on encodings. Textbook examples of valid encoding are the encodings proposed by Boudol and by Honda & Tokoro of the synchronous choice-free $\pi$-calculus into its asynchronous fragment, illustrating that the latter is no less expressive than the former. Here I formally establish that these encodings indeed satisfy Gorla's criteria.