Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. Decoding Choice Encodings
 
research article

Decoding Choice Encodings

Nestmann, Uwe
2000
Journal of Information & Computation

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 defined-equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit decodings from translations to source terms.

  • Details
  • Metrics
Type
research article
DOI
10.1006/inco.2000.2868/pdf
Author(s)
Nestmann, Uwe
Date Issued

2000

Published in
Journal of Information & Computation
Volume

163

Start page

1

End page

59

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LAMP1  
Available on Infoscience
January 24, 2006
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/221725
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés