[moca] Memo on bigraphs

[Robin Milner <Robin.Milner@xxxxxxxxxxxx>]

Dear all

Ole Jensen and I have just finished a memo called "Bigraphs and mobile
processes", which you can find as a Technical Report at

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

It's rather long, but we have broken it up into separate topics
as much as we can (see the abstract below).   We'd be very glad
to hear any comments; please send them to both Ole and me.  

All best wishes
Robin   

--------------------------------------------------------------------

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. 
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html