Computer Laboratory

Technical reports

Bigraphical reactive systems: basic theory

Robin Milner

September 2001, 87 pages

Abstract

A notion of bigraph is proposed as the basis for a model of mobile interaction. A bigraph consists of two independent structures: a topograph representing locality and a monograph representing connectivity. Bigraphs are equipped with reaction rules to form bigraphical reactive systems (BRSs), which include versions of the π-calculus and the ambient calculus. Bigraphs are shown to be a special case of a more abstract notion, wide reactive systems (WRSs), not assuming any particular graphical or other structure but equipped with a notion of width, which expresses that agents, contexts and reactions may all be widely distributed entities.

A behavioural theory is established for WRSs using the categorical notion of relative pushout; it allows labelled transition systems to be derived uniformly, in such a way that familiar behavioural preorders and equivalences, in particular bisimilarity, are congruential under certain conditions. Then the theory of bigraphs is developed, and they are shown to meet these conditions. It is shown that, using certain functors, other WRSs which meet the conditions may also be derived; these may, for example, be forms of BRS with additional structure.

Simple examples of bigraphical systems are discussed; the theory is developed in a number of ways in preparation for deeper application studies.

Full text

PDF (1.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-523,
  author =	 {Milner, Robin},
  title = 	 {{Bigraphical reactive systems: basic theory}},
  year = 	 2001,
  month = 	 sep,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-523.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-523}
}