Stronger Validity Criteria for Encoding Synchrony

TL;DR

This paper evaluates and strengthens the validity criteria for encoding synchrony into asynchrony in the π-calculus, demonstrating that the asynchronous variant is as expressive as the synchronous one under rigorous standards.

Contribution

It introduces stronger validity criteria for encodings and proves the validity of standard translations under these enhanced standards.

Findings

The asynchronous π-calculus is as expressive as the synchronous one.

Standard translations are valid under stronger criteria than previously established.

The paper refines the theoretical understanding of encoding quality in process calculi.

Abstract

We analyse two translations from the synchronous into the asynchronous $\pi$-calculus, both without choice, that are often quoted as standard examples of valid encodings, showing that the asynchronous $\pi$-calculus is just as expressive as the synchronous one. We examine which of the quality criteria for encodings from the literature support the validity of these translations. Moreover, we prove their validity according to much stronger criteria than considered previously in the literature.