[moca] Paper announcement

[Antonio Ravara <Antonio.Ravara@xxxxxxxxxxxxxxx>]

We'd like to announce our paper:

A lexically scoped distributed pi-calculus
by António Ravara, Ana Matos, Vasco T. Vasconcelos, and Luís Lopes,

available at
http://www.di.fc.ul.pt/tech-reports/

Comments are most welcome!
Regards,
antonio


>From the introduction:

Consider a network where we declare a channel "x" within some
site "f", ask for the process x?()P to migrate to
another site "g", and, in parallel launch a receptor
x?()Q located at "x".  Here is the network in Dpi, and the one
obtained after one reduction step.

f[new x (go g. x?()P | x?()Q)] --> new x@f (g[x?()P] || f[x?()Q])

The pertinent questions are: ``where does channel "x" belong to?'',
and ``where is "x" to be stored?''.

Analyzing the "new x@f" part, it would seem that channel "x"
belongs to site "f", but looking at the subnetworks for "g"
and for "f" we cannot really conclude that. More importantly,
we have no clue on where to place the queue for "x", for we have
receptors for "x" at both sites "f" and "g".

We address the above questions by imposing a lexical scope discipline
to networks.  The above left network would reduce to:

new x@f (g [x@f?()P'] || f [x?()Q])

where it is clear that channel "x" belongs to site "f",
and that the queue for "x" should be at "f".

Process "P'" (obtained from "P" by the application of an appropriate
substitution) reflects the fact that "P" has migrated from  "f"
to "g": free simple channels (implicitly located at  "f") become
attached to their site (channel "y" becomes "y@f"); free channels
located at the target site "g" (say "z@g") become simple (by
dropping the "@g" part), reflecting their new local status,
ready for communication; all the remaining channels remain unchanged.


Abstract:
We define the syntax, the operational semantics, and a type system for
lsd-pi, an asynchronous and distributed pi-calculus with local
communication and process migration. The calculus follows a simple model
of distribution for mobile calculi, with a lexical scoping mechanism
that provides both for remote communication and for process migration,
making explicit migration primitives superfluous.
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html