[moca] Technical Report on Bisimulation Congruences for Homer

[Thomas Hildebrandt <hilde@xxxxxx>]

Dear Moca's

We would like to announce the availability of the IT University 
Technical report,
"Bisimulation Congruences for Homer - a calculus of Higher-order mobile 
embedded resources".

It is available at my home page: http://www.itu.dk/people/hilde/pub.htm

Abstract:

We extend Howe's method for proving that late labelled transition 
bisimulations
are congruences to a core process passing calculus with local names,
extended with non-linear active process mobility and
nested locations, as found in the Seal calculus, M-calculus,
and Kell-calculus. The calculus we consider, called Homer for
Higher-order Mobile Embedded Resources, has a very simple syntax and
semantics, which conservatively extend the standard syntax and
semantics for process passing calculi.  The extension of Howe's method
gives a sound characterisation of barbed bisimulation congruence in
terms of a late contextual bisimulation. 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.  We discuss the issue of scope
extension through location boundaries in detail, in particular the
difference between fresh name generation and static local
  names. We propose free name extension as a primitive
construct in calculi with non-linear process mobility, explicit
locations and local names.


Any comments are welcome,

Best regards,
Thomas Hildebrandt
Jens Chr. Godskesen, and
Mikkel Bundgaard

 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html