# zbMATH — the first resource for mathematics

What is a “good” encoding of guarded choice? (English) Zbl 1046.68625
Summary: The $$\pi$$-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the $$\pi$$-calculus with asynchronous output and no choice. This result was recently proved by C. Palamidessi and, as a corollary, she showed that there is no fully compositional encoding from the former into the latter that preserves divergence-freedom and symmetries. This paper argues 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.

##### MSC:
 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: