What Is a ‘Good’ Encoding of Guarded Choice?


  • Uwe Nestmann




The pi-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the pi-calculus with asynchronous output and no choice. As a corollary, Palamidessi recently proved that there is no fully compositional encoding
from the former into the latter that preserves divergence-freedom and symmetries. This paper shows that there are nevertheless `good' encodings between these calculi.
In detail, we present a series of encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice, and investigate them with respect to compositionality and divergence-freedom. The first
and second encoding satisfy all of the above criteria, but various `good' candidates for the third encoding - inspired by an existing distributed implementation - invalidate one or the other criterion. While essentially confirming Palamidessi's result, our study
suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes.




How to Cite

Nestmann, U. (1997). What Is a ‘Good’ Encoding of Guarded Choice?. BRICS Report Series, 4(45). https://doi.org/10.7146/brics.v4i45.19266