Trustworthy Systems

Stronger validity criteria for encoding synchrony


Rob van Glabbeek, Ursula Goltz, Christopher Lippert and Mennicke Stephan


Technical University of Braunschweig

UNSW Sydney


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.

BibTeX Entry

    address          = {Paris},
    author           = {van Glabbeek, Robert and Goltz, Ursula and Lippert, Christopher and Stephan, Mennicke},
    booktitle        = {The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and
                        Privacy --- Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday},
    date             = {2019-11-4},
    doi              = {\_11},
    editor           = {{M.S. Alvim, K. Chatzikokolakis, C. Olarte \& F. Valencia}},
    keywords         = {Process calculi; expressiveness; translations; quality criteria for encodings; valid encodings;
                        compositionality; operational correspondence; semantic equivalences; asynchronous π-calculus.},
    month            = nov,
    pages            = {182-205},
    paperurl         = {},
    publisher        = {Springer},
    series           = {LNCS 11760},
    title            = {Stronger Validity Criteria for Encoding Synchrony},
    volume           = {11760},
    year             = {2019}