[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [moca] Paper: The Kell Calculus: A Family of Higher-Order Distributed Process Calculi
Dear Alan,
I have some questions and remarks for your paper and the Kell calculus.
It looks very interesting - I am sorry that I overlooked the
announcement of the paper (during my vacation :-) in July. I was
recently pointed to it by an anonymous referee.
The Kell calculus shares ideas with a calculus that I and some of my
colleagues (Jens Chr. Godskesen and Mikkel Bundgaard) have been working
on the last two years, called Homer (Higher Order Mobile Embedded
Resources), which builds on the work of the MR calculus of Mobile
Resources (with V. Sassone), presented at CONCUR 2002, essentially
turning the calculus into a more standard, process passing calculus,
greatly simplifying the lts semantics and improving the expressiveness.
Besides both being process-passing calculi, the Kell calculus in
particular shares with Homer the idea of having a located, active
process P as a prefix:
n[P].Q
where Q is activated when P is moved.
We were led to this idea as a generalisation of the normal process
passing, e.g. found in Plain CHOCS. Alse, it generalises both fixed
(persistent) locations (since Q may model an empty location) as found
in Ambients and MR, and locations that dissapears, or get inaccessible,
when the resource is moved, e.g. as seals in the Seal calculus. (It
also solves a problem in the Seal calculus, that the movement of seals
can not be observed).
Where you led by similar ideas?
Our motivation for introducing Homer has NOT been to propose it as a
general-purpose model for mobile computing processes, but rather to
study the problem of characterising congruences for higher-order,
non-linear mobile computing processes with nested locations
co-inductively by labelled transition bisimulations. Finding a sound
and complete characterisation for such a higher-order calculus with
locations is (as you know) a hard problem. So far, we have only a sound
characterisation. (as far I am aware, this is also the status for the
Seal calculus. Sound and complete characterisations exist for the
Ambient calculus, but the Ambient calculus does not allow mobile
computing resources to be copied.)
Even the sound characterisation required quite some work to get - it
involved a non-trivial generalisation of Howe's method to nested
locations.
As far as I can see, your lts characterisation of barbed congruence
contains a serious mistake, namely that you consider reaction and lts
semantics for #open# terms but only define the lts bisimulation for
closed terms (and extend it to the congrurence by closing under
subsitutions). This makes the arguments used in the Sketch of Theorem 3
wrong. You can not use the result that tau-transitions and reactions
conincide to infer that the lts bisimulation is included in the barbed
bisimulation when the lts bisimulation is only defined for closed
terms.
Are you aware of this? or have I overlooked something?
In a very early version of Homer (dating back to early 2003) we
considered a similar semantics, but discarded it for that reason. Also,
at least to me, it seems questionable to allow open terms to reduce and
processes later can be substituted for the variable, as long as the
input prefix is passivating the residual: In any context, a process can
only be substituted for a process variable in a term that appears
behind an input prefix, thus the open process can not perform reaction
steps before all of its variables have been substituted for processes.
I would be very interested in hearing your opinion - and if you have
ideas on how to solve this problem.
A full description of Homer and the sound characterisation of barbed
congruence has not yet appeared in print in a public version (partly
because we have struggled with finding a complete characterisation),
however, a technical report including the sound characterisation on
Homer is getting finalized and will appear in a few weeks.
A (simplified) version of Homer was presented at EXPRESS this year. The
paper, titled "A CPS encoding of Name-passing in Higher Order Mobile
Resources", shows that even a restricted version of Homer allows an
encoding of pi-calculus name passing and substitution, clearly showing
the strenght of being able to indirectly address (anonyomous) processes
at named locations. However, the paper does not contain the lts
semantics and thus does not consider the (hard) problem of
characterising barbed congruence co-inductively.
A version of Homer was also presented at the International Workshop for
Formal Methods and Security in Nanjing in April, describing a type
system for distinguishing between linear and non-linear (e.g. copyable)
mobile processes.
Best regards,
Thomas Hildebrandt
IT University of Copenhagen
On 21/7-2004, at 11.59, Alan Schmitt wrote:
Dear all,
We are pleased to announce the following paper, to appear in the LNCS
volume of the post-proceedings of the Global Computing 2004 workshop,
and available at
http://sardes.inrialpes.fr/~aschmitt/papers/LNCS_GC_04_Kells.ps.gz
Comments are welcome.
The Kell Calculus: A Family of Higher-Order Distributed Process Calculi
This paper presents the Kell calculus, a family of distributed process
calculi, parameterized by languages for input patterns, that is
intended
as a basis for studying component-based distributed programming. The
Kell calculus is built around a pi-calculus core, and follows five
design principles which are essential for a foundational model of
distributed and mobile programming: hierarchical localities, local
actions, higher-order communication, programmable membranes, and
dynamic
binding. The paper discusses these principles, and defines the syntax
and operational semantics common to all calculi in the Kell calculus
family. The paper provides a co-inductive characterization of
contextual equivalence for Kell calculi, under sufficient conditions on
pattern languages, by means of a form of higher-order bisimulation
called strong context bisimulation. The paper also contains several
examples that illustrate the expressive power of Kell calculi.
Best regards,
Alan Schmitt
Jean-Bernard Stefani
--
The hacker: someone who figured things out and made something cool
happen.
.O.
..O
OOO
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html