Decoding choice encodings

We study two encodings of the asynchronous pi -calculus with input-guarded choice into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is f ully abstract with respect to weak bisimulation, but the more natural diver gence-free encoding is not. instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser-but still coinductively defined-equivalence that does not enforce bisimilarity of internal branchin g decisions. The correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit decodings fro m translations to source terms. (C) 2000 Academic Press.