Bigraphical Reactive Systems

Forty years ago, Carl-Adam Petri devised the first substantial model of concurrent computation, and it was a graphical model. Since then there has been a steady flow of models and calculi in which the spatial metaphor is never far away; we often use terms like linkage, location, mobility, and so on.

The flow is increasing, with the challenge to understand mobility, security, and other properties of virtual and real networks. We shall soon have as many calculi as programming languages. I believe that the only way to achieve some unity is to represent connectivity and locality graphically, in an unconstrained form upon which different specific calculi can impose finer or stricter structure.

In the talk I shall describe bigraphs, which arise from the pi calculus, the ambient calculus and action calculi; they treat connectivity and locality orthogonally ("where you are does not affect who you can talk to"). I shall show with examples how the model specialises to familiar calculi. I shall also explain how the general theory of bigraphs uniformly yields labelled transition systems for which many behavioural relations - like bisimilarity - are necessarily congruential. So bigraphs not only give a framework for a variety of models, but also provide a core theory which they can all use.

The talk will not presuppose any knowledge of calculi for concurrency.