UCAM-CL-TR-570: Bigraphs and mobile processes

Publication announcement:

    Bigraphs and mobile processes

    Ole Hogh Jensen, Robin Milner

    Technical report UCAM-CL-TR-570, University of Cambridge,
    Computer Laboratory, July 2003, 121 pages.

This document is now available at

    http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-570.pdf

Abstract:

A bigraphical reactive system (BRS) involves bigraphs, in which the
nesting of nodes represents locality, independently of the edges
connecting them; it also allows bigraphs to reconfigure themselves. BRSs
aim to provide a uniform way to model spatially distributed systems that
both compute and communicate. In this memorandum we develop their static
and dynamic theory.

In Part I we illustrate bigraphs in action, and show how they correspond
to to process calculi. We then develop the abstract (non-graphical)
notion of wide reactive system (WRS), of which BRSs are an instance.
Starting from reaction rules --often called rewriting rules-- we use the
RPO theory of Leifer and Milner to derive (labelled) transition systems
for WRSs, in a way that leads automatically to behavioural congruences.

In Part II we develop bigraphs and BRSs formally. The theory is based
directly on graphs, not on syntax. Key results in the static theory are
that sufficient RPOs exist (enabling the results of Part I to be
applied), that parallel combinators familiar from process calculi may be
defined, and that a complete algebraic theory exists at least for pure
bigraphs (those without binding). Key aspects in the dynamic theory
--the BRSs-- are the definition of parametric reaction rules that may
replicate or discard parameters, and the full application of the
behavioural theory of Part I.

In Part III we introduce a special class: the simple BRSs. These admit
encodings of many process calculi, including the pi-calculus and the
ambient calculus. A still narrower class, the basic BRSs, admits an easy
characterisation of our derived transition systems. We exploit this in a
case study for an asynchronous pi-calculus. We show that structural
congruence of process terms corresponds to equality of the representing
bigraphs, and that classical strong bisimilarity corresponds to
bisimilarity of bigraphs. At the end, we explore several directions for
further work.

-- 
University of Cambridge, Computer Laboratory,
Technical Reports (ISSN 1476-2986)
http://www.cl.cam.ac.uk/TechReports/