Decoding Choice Encodings

by Uwe Nestmann, INRIA Rocquencourt, France and Benjamin C. Pierce, Indiana University, USA

August 11, 1997

Abstract

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 fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser - but still coinductively designed - equivalence that does not enforce bisimilarity of internal branching decisions. The rigorous correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit decodings from translations to source terms.

Interested?

gziped PostScript file (use the "load to disc" option)
PDF file (For PDF files, a free viewer (Acrobat Reader) is available from Adobe Systems.

return to the research reports content list