Stronger Validity Criteria for Encoding Synchrony

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.

Written in 2019. Dedicated to Catuscia Palamidessi, on the occasion of her 60th birthday

References in corpus (7)

• Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculi
• Musings on Encodings and Expressiveness
• Analysing and Comparing Encodability Criteria
• Synchrony vs Causality in the Asynchronous Pi-Calculus
• On the Expressiveness of Intensional Communication
• On the Expressiveness of Joining
• A Theory of Encodings and Expressiveness

Cited by in corpus (2)

• Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
• Minimal Translations from Synchronous Communication to Synchronizing Locks