Computer Laboratory

Technical reports

Bigraphs and mobile processes

Ole Høgh Jensen, Robin Milner

July 2003, 121 pages

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 π-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 π-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.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-570,
  author =	 {Jensen, Ole H{\o}gh and Milner, Robin},
  title = 	 {{Bigraphs and mobile processes}},
  year = 	 2003,
  month = 	 jul,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-570.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-570}
}