Stronger Validity Criteria for Encoding Synchrony
Rob van Glabbeek, Ursula Goltz, Christopher Lippert, Stephan Mennicke
TL;DR
This paper re-evaluates two canonical encodings of the synchronous into the asynchronous $π$-calculus, using Gorla's framework and stronger semantic-equivalence notions to assess validity. It shows that Boudol's encoding is valid under a robust, divergence-preserving, success-respecting form of weak reduction bisimilarity, aligning with established encodability criteria, while Honda & Tokoro's encoding is not valid under standard weak equivalences but becomes valid under a newly proposed weak channel bisimilarity that abstracts away input/output distinctions. The results clarify the relative strength of these encodings and deepen understanding of expressiveness in the $π$-calculus, guiding their use in formal verification and semantic reasoning. Overall, the work advances the theory of encodings between concurrent calculi and informs when stronger versus weaker equivalence notions are appropriate for validating encodings.
Abstract
We analyse two translations from the synchronous into the asynchronous $π$-calculus, both without choice, that are often quoted as standard examples of valid encodings, showing that the asynchronous $π$-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.