Separation of synchronous and asynchronous communication via testing

Research output: Contribution to journalArticlepeer-review

Abstract

One of the early results concerning the asynchronous π-calculus which significantly contributed to its popularity is the capability of encoding the output prefix of the (choiceless) π-calculus in a natural and elegant way. Encodings of this kind were proposed by Honda and Tokoro, by Nestmann and (independently) by Boudol. We investigate whether the above encodings preserve De Nicola and Hennessy's testing semantics. In this sense, it turns out that, under some general conditions, no encoding of the output prefix is able to preserve the must testing. This negative result is due to (a) the non-atomicity of the sequences of steps which are necessary in the asynchronous π-calculus to mimic synchronous communication, and (b) testing semantics' sensitivity to divergence.

Original languageEnglish
Pages (from-to)218-235
Number of pages18
JournalTheoretical Computer Science
Volume386
Issue number3
DOIs
Publication statusPublished - 1 Nov 2007
Externally publishedYes

Keywords

  • Asynchronous π-calculus
  • Encoding
  • Synchronous communication
  • Testing semantics

Fingerprint

Dive into the research topics of 'Separation of synchronous and asynchronous communication via testing'. Together they form a unique fingerprint.

Cite this