Hi Thomas, First of all, thanks a lot for your comments and questions. To make the conversation easier to follow, I will answer your message inline. * Thomas Hildebrandt (hilde@xxxxxx) wrote: > 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. We knew of the calculus of Mobile Resources, but not of Homer. We'll definitely have a look at it. > > 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? Not really. Our main motivation is to create a calculus that may model components (in the sense of hierarchical encapsulated units of computation) and their environment (to study deployment and failure of components). We decided to design a higher-order calculus because the properties we want to study are definitely higher-order. The synchronous aspect (having continuations to messages and locations that are consumed) is indeed used to observe these actions, but was not central in the design of the calculus. > > 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. 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. > > 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. > > 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. I agree with you that allowing the reduction of open terms is questionable, and may lead to strange things. However, our definitions for strong barbed congruence and strong context congruence rely on the closed congruences (intuitively by saying that the considered processes are still bisimilar whichever way one closes them), and even though the transition systems are defined for any process, when doing congruence proofs they are only used with closed processes. 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. > > 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. Best regards, Alan Schmitt Jean-Bernard Stefani -- The hacker: someone who figured things out and made something cool happen. .O. ..O OOO
Attachment:
pgpNFHtv3sycd.pgp
Description: PGP signature