The calculus of Higher-order Mobile Embedded Resources (Homer)

The calculus of Higher-order Mobile Embedded Resources (Homer) is a pure (non-linear) higher-order calculus with mobile computing processes in nested locations, defined as a simple, conservative extension of the core process-passing subset of Thomsen's Plain CHOCS[Tho93]. The calculus is defined such that it has very simple syntax and semantics, which conservatively extend the standard syntax and semantics for process passing calculi. The nested names as location addresses, as found in nested name spaces of distributed systems, where introduced in the predecessor of Homer, the calculus of Mobile Resources (MR) [GHS02]. The (untyped) Homer calculus presented in [HGB04a] contains a novel process constructor, inspired by bigraphs, called free name extension, which extends the set of free names with an idle name. This is one way of solving the problems related to scope extension in process calculi with non-linear process mobility and local names, which have also been observed in similar calculi, such as the Seal calculus and the Kell calculus. In [GH05] we give an equivalent presentation in the form of a typed version of the Homer calculus.

In [HGB04a] we have proved that late labelled transition bisimulations are congruences using Howe's method. Hence, we have a sound characterisation of barbed bisimulation congruence in terms of a late contextual bisimulation. Furthermore, we show that early contextual bisimulation is complete with respect to barbed bisimulation congruence, but that the late bisimulation is in fact strictly included in the early bisimulation.

In [GH05] we have extended the result to prove that input-early (strong and delay) labelled transition bisimulations are congruences using Howe's method. This gives again sound characterisations of strong and weak barbed bisimulation congruence, which is also complete in the case of strong bisimulation.

In [BHG04] we present an encoding of the synchronous pi-calculus in Homer. The encoding is fully abstract wrt. barbed bisimulation and sound wrt. barbed congruence. This encoding demonstrates that higher-order process-passing together with mobile computing resources in (local) named locations are sufficient to express pi-calculus name-passing.

In [BH05] we provide a bigraphical presentation of Homer (with explicit substitutions) and its reaction semantics. We prove that structural congruence of Homer corresponds to graph isomorphism in its bigraphical representation and that there is a tight operational correspondence between the reaction relation of Homer and the reaction rules in the bigraphical representation. The presentation highlights the importance of keeping explicit track of the free names of parameters in reaction rules of bigraphs. It also addresses the issue of localisation of names (links) which suggests an extension to local bigraphs called bigraphs with localised links.

Future Work

• From the Bigraphical presentation of Homer in [BH05] we can derive a labelled bisimulation congruence. We plan to investigate this bisimulation semantics, compare it to the ad-hoc semantics and investigate bisimulation proof techniques in this setting.
• It is still an open problem to give a sound and complete characterisation of a weak barbed bisimulation congruence for Homer. We are currently investigating a notion of delay-barbed bisimulation corresponding to the input-early delay contextual bisimulation congruence provided in [GH05].

References

• [Tho93] B. Thomsen. Plain CHOCS: A second generation calculus for higher order processes . Acta Informatica, 30(1):1--59, 1993.
• [GHS02] J. C. Godskesen, T. Hildebrandt, and V. Sassone. A Calculus of Mobile Resources. In L. Brim, P. Jancar, M. Kretinsky, and A. Kucera, editors, Proceedings of the 13th International Conference on Concurrency Theory (CONCUR'02), volume 2421 of LNCS, pages 272--287. Springer Verlag, 2002.
• [GH03] J. C. Godskesen, T. Hildebrandt. Copyability Types for Mobile Computing Resources. International Workshop on Formal Methods and Security, 2003, Nanjing, China.
• [BHG04] M. Bundgaard, T. Hildebrandt, and J. C. Godskesen. A CPS Encoding of Name-passing in Higher-Order Mobile Embedded Resources. In Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS'04), ENTCS. Elsevier, 2004. (pdf and ps)
• [HGB04a] T. Hildebrandt, J. C. Godskesen, and M. Bundgaard. Bisimulation Congruences for Homer - a Calculus of Higher Order Mobile Embedded Resources. Technical Report TR-2004-52, IT University of Copenhagen, 2004. (pdf and ps)
• [GH05] J. C. Godskesen and T. Hildebrandt Extending Howe's Method to Early Bisimulations for Typed Mobile Embedded Resources with Local Names. In Proceedings of FSTTCS'2005, volume 3821 of Lecture Notes in Computer Science, pages 140--151. Springer Verlag. june 2005.
• [BH05] M. Bundgaard and T. Hildebrandt Bigraphical Semantics of Higher Order Mobile Embedded Resources with Local Names. In Proceedings of the Graph Transformation for Verification and Concurrency workshop (GT-VC'05), volume 154(2) of Electronic Notes in Theoretical Computer Science, pages 7-29. Elsevier, 2006. (pdf)
• [BHG07] Mikkel Bundgaard, Thomas Hildebrandt, and Jens Chr. Godskesen. Modelling the security of smart cards by hard and soft types for higher-order mobile embedded resources. In Proceedings of the 5th International Workshop on Security Issues in Concurrency (SecCo'07), volume 194(1) of Electronic Notes in Theoretical Computer Science, pages 23-38. Elsevier, 2007. (pdf, full version)

last updated November 2007