[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

Hi Alan,

thank you for your reply, the typo does explain some of my confusion, but I am still a bit puzzled
exactly which definitions that contain typos, maybe you can clarify that for me. 


Surprisingly enough, we did not know Howe's method when we started
working on bisimulations for the Kell Calculus. As generalizing it to
nested locations seemed as hard as the approach we were using, we did
not pursue it.


I can recommend the presentation of Baldamus and Frauenstein. It can be found online in a technical report 95-21 from Berlin University of Technology, 1995.

(We are right now working on an extension of the method to early bisimulations, which would
provide a sound and complete characterisation of the barbed congruence for Homer.)


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? 

Both lts bisimulation and barbed bisimulation are defined on closed
terms (there was a typo in the definition of barbed bisimulation where
the process was not closed before being put in the closed context, this
might have been the source of the confusion).

For the inclusion of ~c in ~cb (lts congruence in barbed congruence),
the reasonning is the following:
- we have ~ in ~b (both are closed) by Theorem 1 (the lts and reduction
coincide), as the reduction / transition of a closed term is a closed
term.
- we have ~ in ~c (this is immediate as ~c is the extension of ~ to open
terms), and ~ is a congruence (because ~c is, Theorem 2, and
considering any closed context)
- assume P ~c Q. Let s be a substitution that closes P and Q, and let K
be a closed context. We need to show that K(Ps) ~b K(Qs) to conclude.
First, by definition of ~c, we have Ps ~ Qs, hence K(Ps) ~ K(Qs) as ~
is a congruence, hence K(Ps) ~b K(Qs) by inclusion of ~ in ~b.

Does this clarify things ? We will soon put an updated version online
that clarifies this and a few other things.



It do clarify some things... But just to be precise:

- you change the definition of barbed bisimulation ~b to closed terms (Def. 8).

- you change the definition of barbed congruence (Def. 9) such that you close the two processes
before inserting them in a closed context, i.e. two open processes P and Q, define P~bc Q if
for all closing substitutions s, and all closed contexts K, K(Ps)~b K(Qs).

If that is the case it looks consistent with what you write below.

However, then I can not see that ~bc is the largest congruence included in ~b (as you state in proposition 2). ~bc is defined on open terms and ~b is defined on closed terms, right?

Clearly ~bc is included in the open extension ~bo of ~b defined by P~bo Q if for all closing substitutions s it holds that Ps~b Qs.
But I can not convince my self that ~bc is a congruence in the usual sense, i.e. is it a congruence wrt input prefix on open terms?? That is, if P~bc Q are two open terms, will a<x> >P and a<x> > Q be related?

Maybe I am just still confused about what the definitions exactly are....
We have not yet considered an open version of the calculus, where
bisimulations would not need to consider all the ways to close the
processes. I think it is a fairly hard problem, and we have decided to
work first on normal bisimulations, which is somehow related as we're
introducing a calculus with a notion of resource (represented by a name)
that may be substituted by the corresponding process at any time. This
work on normal bisimulations is still in progress, and we have not
published it yet.


I agree that it would be very interesting in getting normal bisimulations extended to calculi
with locations.This is also one of our current topics for Homer.



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. 

We will have a look at these papers. Thanks for pointing them out.


Only the EXPRESS paper is available so far. The others may be available in old versions, but I would recommend waiting for the technical report to come within the next 10 days..., since the others do contain bugs.

Best,
Thomas

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