首页    期刊浏览 2024年11月13日 星期三
登录注册

文章基本信息

  • 标题:Decoding Choice Encodings
  • 本地全文:下载
  • 作者:Uwe Nestmann ; Benjamin C. Pierce
  • 期刊名称:BRICS Report Series
  • 印刷版ISSN:0909-0878
  • 出版年度:1999
  • 卷号:6
  • 期号:42
  • 出版社:Aarhus University
  • 摘要: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.
国家哲学社会科学文献中心版权所有