A Brief Introduction To Bigraphs

From PLSwiki

Jump to: navigation, search

Contents

Introduction

A bigraph is a mathematical structure consisting of two graphs, a place graph and a link graph, intended for modelling distributed, mobile systems.

Why do I need to model systems?

When designing a system consisting of more than one component (be it distributed or not) it is typically a good idea to sketch the structure and interaction patterns of the system.

Even when programming smaller applications it might be a good idea to draw the structure of the program, spelling out the dependencies between different subcomponents of the program.

For example, you might use UML diagrams to show the inheritance structure for a Java or a C++ program. Or you might write down an expression in a process calculus to model the behavior of a concurrent system.

Making models typically helps you get a more clear picture of properties of the system - things like what communication is actually happening between which components, and which components are not communicating. You might also specify that some components are not allowed to communicate, or that some action is not allowed to happen in a system.

The nice thing about formal models are that they typically give you some machinery to actually prove that such properties hold in (a model of) a system.

So what is a bigraph?

A bigraph B consists of two graphs (hence the name) - a place graph and a link graph - sharing nodes. The place graph is restricted to be a tree (no cycles), while the link graph can be a hypergraph, i.e., a link can connect more than two objects. Each of these subgraphs can be pictured individually, like this:

Image:introLinkPlacegraph.png

The shared nodes are labelled v_i.

By representing both components of the bigraph in one picture, we can get an impression of object locations and connections simultaneously:

Image:introBigraph.png

Here the place graph is represented by placing nodes inside each other according to the parent relation of the place graph, while edges of the link graph are still simply connected to the nodes. Each node is assigned a control (think of it as a 'kind' or 'type'), specifying the number of ports to which we can attach links.

The r_i's in the place graph - called roots - are translated into outermost containing frames, and the s_i's - called sites - are displayed as innermost gray boxes.

The corresponding structure in the link graph - the y_i's and the x_i's - are called outer and inner names, respectively.

The roots and the outer names make up the outer face of the bigraph, while the sites and the inner names make up its inner face. Inner and outer faces are referred to collectively as interfaces. In the preceding example, we could express B's interfaces by writing B : 〈3,{x0,x1}〉 → 〈2,{y0,y1,y2}〉, indicating that B has 3 sites and inner names x0, x1, and 2 roots and outer names y0, y1, y2.

Bigraphs are compositional structures - the sites of the bigraph work like holes, into which other bigraphs can be inserted.

Interfaces tell us which bigraphs can be composed. We can only insert a bigraph A into another bigraph B (written B o A), if the inner face of B is identical to the outer face of A. In other words we must require A : I → I' and B : I' → J for some interfaces I, I', J.

So we could for instance insert a bigraph with 3 roots and the outer names x1, x2 into the bigraph B.

Or we could construct the bigraph B by composing the bigraphs C and D below:

Image:introComposeBigraph1.png

Image:introComposeBigraph2.png

We write B = D o C to express that C inserted into D is equal to the bigraph B.

How do I model systems with bigraphs?

The idea is to model the locational structure of the system with the place graph. This explains why the place graph is tree-structured - the topography of a system can usually be modelled as a set of domains or objects contained within each other.

Connections between objects or domains are modelled by links. For example this might simply model that a number of entities connected via a link are able to communicate with each other.

Let's take a look at a small, but very concrete example system modelled in bigraphs. (This system is inspired by the DELCA project currently running at ITU - see delca.itu.dk) :

Image:ghostBigraph1.png

This system is a model of a simplified ITU with a few rooms modelled by Room nodes. (As this bigraph has only one root we've left out the frame.) Each Room has a single port that links it to a number of Door nodes (you can probably guess what they model...)

In one of the Rooms a Ghost node resides alongside a Person node and a PC node. The idea is that this Ghost node models a butler Ghost that can accompany the Person to another Person, located in one of the other Rooms.

Note that there are no sites or outer or inner names in this system. This means that we can't insert other bigraphs into this system, and if we were to embed this model of ITU into a greater bigraph, there would be no linkage between ITU and the surroundings.

But this is just a model of a static system. Even though we've stated that the intention is that the Ghost should somehow connect with a Person and accommpany that Person somewhere, the model says nothing about this. The picture only shows the current state of the system. So clearly something is missing...

As hinted upon, what we would like to do, is to also be able to specify the dynamics of the system within the model.

This can also be done using bigraphs. We can specify Bigraphical Reactive Systems (BRS's) by defining a set of reaction rules. A reaction rule is a pair of bigraphs, redex and reactum where the redex defines a pattern to be matched with a bigraph modelling the current state of a system. A reaction is simply the substitution of a redex with a reactum.

The following pictures shows a few simple reaction rules, Connect and Move, that specify allowed changes in the model:

Image:ghostBigraph2.png

In words, the Connect reaction rule tells us that: "When a Person and a Ghost is in the same Room, connected to an unspecified set of Doors, the Ghost can 'connect' with the Person". Here we have modelled a 'connect' by inserting the Person node into the Ghost node. We could specify a Disconnect rule simply by inverting the reaction arrow, that would tell us the opposite, namely that a Ghost and a Person inside a Room (with similar properties) can also 'disconnect'.

The following rule allows a Ghost node containing a Person node to move from one Room to the next, provided they are connected by the same Door:

Image:ghostBigraph3.png

Note that the sites allow that the Rooms contain other things besides the Ghost and Person nodes. Furthermore, the outer names doorlink (and doorlink_i) allow the Rooms to have an arbitrary number of Doors.

This actually makes the rules more like rule schemas in that they specify a set of situations where a reaction could occur: For example, we get an instance of the Connect rule, if we plug in a parameter bigraph p (representing other objects in the room) into the site of the redex, and plug the redex into a context - a bigraph E_c representing the surroundings.

So a reaction in our concrete system using the Connect rule requires us to produce an instance of the Connect rule, that would match our modelled system exactly. Specifically, that would be a parameter bigraph p that is simply a frame with a PC node inside. The context bigraph E_c has a single site and one inner name called doorlink, that is linked to the dlob link. It is depicted in the following picture:

Image:ghostBigraph4.png

The relation between the system before and after the reaction is precisely recorded in the equality: Ec o Rc o p = Ec o Rc' o p.

This means that the Connect reaction rule allows us to infer that in our concrete model of ITU, a specific Person and a specific Ghost can connect with each other.

And what has this got to do with programming?

As mentioned in the introduction, modelling languages need not be graphical like UML or bigraphs. If you have dabbled with modelling concurrent or mobile systems you might have stumbled upon calculi like the CCS or the pi calculus.

In these modelling languages we write terms not unlike in a simplified programming language, and they are called calculi exactly, because we have relatively simple ways of 'calculating' the behavior of systems, we model in them.

Some programs actually allow you to derive UML diagrams from your Java or C++ code; or they might allow you to draw the diagrams and then generate some stub code for you that saves you a lot of typing - apart from having to check that your code actually corresponds to your model!

Clearly, there are some gains in being able to translate directly (perhaps even back and forth!) from model to actual code.

In the BPL project we are currently working on developing a syntax and an interpreter for bigraphs and bigraphical reactive systems, so that we can specify models, like the one in the previous section, in a language that looks like a regular programming language; and 'run' them - by allowing reactions to occur in the system.

One of the main goals of the BPL project is to experiment with how actual programming languages for programming distributed and mobile systems based on the theory of bigraphs can be constructed.

For example, the 'bigraph program' might translate into stub code to place on servers and clients that handles messages and distribution of code and data. When 'filling in the content' of the system, the developer would then be presented with a simple interface for managing the distribution and mobility in the system - in a way the 'infrastructure' of the system would be delivered by the (translation of the) bigraphical model.

Again, this automatic generation of code would also ensure the developer that the code that implements the model actually corresponds to the model; so any properties he proved for the model - e.g. that a deadlock can never occur - would also hold for the actual implementation.

Or maybe a general programming language, like Java or C++ - but especially directed towards programming small applications for mobile phones, could be based on bigraphs.

Furthermore, we are currently also investigating connections between XML and bigraphs. XML and bigraphs share the property of being a general model in which both statics and dynamics can be modelled. In particular, we are working on an XML representation of bigraphs and bigraphical reactive systems.

We also hope to base a picture generator that generates pictures, like the ones above, upon a suitable XML representation.

Personal tools