Mobile Processes in Bigraphs
Download: Jensen-monograph.pdf (1.2 MB)
Abstract
Bigraphical reactive systems (BRSs) are a formalism for modelling mobile computation. A bigraph consists of two combined mathematical structures: a place graph that models locality, and a link graph that models connectivity. The computation, or behaviour, of systems is modelled as reaction rules that prescribe how bigraphs can change dynamically. A notion of bisimulation exists for BRSs, based on a notion of contextual transitions derived uniformly from any given set of reaction rules.
In this dissertation we make several extensions to the theory of bigraphs and give two substantial applications, demonstrating how two of the main existing models of mobile computation, the pi-calculus and the ambient calculus, can be accurately represented as particular instances of BRSs.
One of our extensions is place-sorting, a refinement of bigraphs that allows certain structural constraints to be imposed. As another extension we refine the existing notion of (strong) bisimilarity into weak bisimilarity, closely following the spirit of the similar well-known concept in process calculi; we show how, for contextual transitions, weak bisimilarity can be based elegantly on a method for composing reaction rules. Our third main extension to the theory of bigraphs concerns the adequacy (for proving bisimilarity) of a subclass of the contextual transitions known as engaged transitions; we extend previous adequacy theorems to cover a wider range of BRSs, in particular including certain BRSs in which sub-systems can be replicated dynamically.
Our first application of bigraphs demonstrates how (several versions of) the pi-calculus can be modelled in a way that accurately represents both the structure and the dynamics of processes. We investigate the contextual transitions (and accompanying bisimilarity) induced on the calculus by the bigraph model, and in particular we compare them to the original transition systems and bisimilarities defined specifically for the calculus, finding substantial (though not complete) agreement. We repeat the exercise for the ambient cal culus (mobile ambients), obtaining similar results.