[moca] full version of paper on expressiveness of pi vs. asynchronous pi

[Catuscia Palamidessi <catuscia@xxxxxxxxxxx>]

Hi, 

For those who are interested, the full version of my paper on the comparison
between the expressive power of the synchronous and asynchronous pi-calculus is
now available at the following address:

   http://www.cse.psu.edu/~catuscia/papers/pi_calc/mscs.ps

With respect to the conference version (POPL 97) this full version contains a
separation result between the pi-calculus and the pi-calculus with internal
mobility proposed by Sangiorgi. Also, the proofs are worked out in more detail
and some definitions have been formulated more precisely.

The abstract is enclosed below.

Best regards, Catuscia

-----------------------------------------------------------

Title: Comparing the Expressive Power of the Synchronous and the Asynchronous pi
calculus 

Author: Catuscia Palamidessi

Status: To appear on MSCS, in a special issue dedicated to Expressiveness of
concurrent languages, edited by Luca Aceto, Peppe Longo, and Bjorn Victor.

Abstract:
The Asynchronous $\pi$-calculus, proposed by Honda and Tokoro (1991) and,
independently, by Boudol (1992), is a subset of the $\pi$-calculus which
contains no explicit operators for choice and output-prefixing. The
communication mechanism of this calculus, however, is powerful enough to
simulate output-prefixing, as shown by Honda and Tokoro (1991) and by Boudol
(1992), and input-guarded choice, as shown by Nestmann and Pierce (2000). A
natural question arises, then, whether or not it is as expressive as the full
$\pi$-calculus. We show that this is not the case. More precisely, we show that
there does not exist any uniform, fully distributed translation from the
$\pi$-calculus into the asynchronous $\pi$-calculus, up to any ``reasonable''
notion of equivalence. This result is based on the incapability of the
asynchronous $\pi$-calculus to break certain symmetries possibly present in the
initial communication graph. By similar arguments, we prove a separation result
between the $\pi$-calculus and CCS, 
and between the $\pi$-calculus and the $\pi$-calculus with internal mobility, a
subset of the $\pi$-calculus proposed by Sangiorgi where the output actions can
only transmit private names.

-----------------------------------------------------------
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html