On Equators in Asynchronous Name-passing Calculi without Matching – Extended Abstract –
Massimo Merro · Electronic Notes in Theoretical Computer Science · 1999
We give a labeled characterization of barbed congruence in asynchronous π-calculus, which, unlike previous characterizations, does not use the matching construct. In absence of matching the observer cannot directly distinguish two names. In asynchronous π-calculus the fact that two names are indistinguishable can be modeled by means of Honda and Yoshida's notion of equator. Our labeled characterization is based on such a notion. As an application of our theory we provide a fully abstract encoding w.r.t. barbed congruence of external mobility (communication of free names) in terms of internal mobility (communication of private names).