Bisimulation Congruences in Safe Ambients (extended abstract).
Citation:
Massimo Merro and Matthew Hennessy., Bisimulation Congruences in Safe Ambients (extended abstract)., Conference Record of POPL '02: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002, 71-80Download Item:
Bisimulation.pdf (Published (author's copy) - Peer Reviewed) 425.3Kb
Abstract:
We develop a semantics theory for SAP, a variant of Levi and Sangiorgi?s Safe Ambients, SA.
The dynamics of SA relies upon capabilities (and co-capabilities) exercised by mobile agents,
called ambients, to interact with each other. These capabilities contain references, the names of
ambients with which they wish to interact. In SAP we generalise the notion of capability: in
order to interact with an ambient n, an ambient m must exercise a capability indicating both n
and a password h to access n; the interaction between n and m takes place only if n is willing to
perform a corresponding co-capability with the same password h. The name h can also be looked
upon as a port to access ambient n via port h.
In SAP by managing passwords/ports, for example generating new ones and distributing them
selectively, an ambient may now program who may migrate into its computation space, and when.
Moreover in SAP an ambient may provide different services/resources depending on the port
accessed by the incoming clients. Then, we give an lts-based operational semantics for SAP and
a labelled bisimulation equivalence which is proved to coincide with reduction barbed congruence.
We use our notion of bisimulation to prove a set of algebraic laws which are subsequently
exploited to prove more significant examples.
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PUBLISHED
Author: HENNESSY, MATTHEW
Type of material:
Conference PaperAvailability:
Full text availableKeywords:
Computer science, Mobile agents, distributed systems, bisimulationLicences: