Bisimulation Congruences for Homer: a Calculus of Higher Order Mobile Embedded Resources

Thomas Hildebrandt, Jens Christian Godskesen, Mikkel Bundgaard

Research output: Book / Anthology / Report / Ph.D. thesisReportResearch

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.
Original languageEnglish
Place of PublicationCopenhagen
PublisherIT-Universitetet i København
EditionTR-2004-52
Number of pages25
ISBN (Electronic)87-7949-074-3
Publication statusPublished - Oct 2004
Externally publishedYes
SeriesIT University Technical Report Series
NumberTR-2004-52
ISSN1600-6100

Fingerprint

Dive into the research topics of 'Bisimulation Congruences for Homer: a Calculus of Higher Order Mobile Embedded Resources'. Together they form a unique fingerprint.

Cite this