Bisimulation Congruences for Homer - a Calculus of Higher Order Mobile Embedded Resources
TR-2004-52, Authors: Thomas Hildebrandt, Jens Chr. Godskesen and Mikkel Bundgaard
Bisimulation Congruences for Homer - a Calculus of Higher Order Mobile Embedded Resources
October 2004
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.
Technical report TR-2004-52 in IT University Technical Report Series,
October 2004.
Available as PDF.