Trustworthy Systems

A theory of encodings and expressiveness


Rob van Glabbeek


UNSW Sydney


This paper proposes a definition of what it means for one system description language to encode another one, thereby enabling an ordering of system description languages with respect to expressive power. I compare the proposed definition with other definitions of encoding and expressiveness found in the literature, and illustrate it on a well-known case study: the encoding of the synchronous in the asynchronous π-calculus.

BibTeX Entry

    address          = {Thessaloniki, Greece},
    author           = {van Glabbeek, Robert},
    booktitle        = {Proceedings of the  21st International Conference on Foundations of Software Science and
                        Computational Structures},
    date             = {2018-4-14},
    doi              = {\_10},
    editor           = {{Baier, Christel Baier and Dal Lago, Ugo}},
    keywords         = {Expressiveness; encodings; languages; translations; compositionality; semantic equivalences;
    month            = apr,
    pages            = {183-202},
    paperurl         = {},
    publisher        = {Springer},
    series           = {Lecture Notes in Computer Science},
    title            = {{A} Theory of Encodings and Expressiveness},
    volume           = {10803},
    year             = {2018}