Bigraphs and Mobile Processes

Robin Milner

Computer Laboratory

Description

The pi calculus is a process calculus that allows processes to manipulate their own connectivity. Another process calculus -- Mobile Ambients (Cardelli and Gordon) -- allows processes to manipulate their own locality. The two seem complementary. Bigraphs are so-called because they rest on two graphical structures that treat connectivity and locality as independently as possible. The behavioural theory of bigraphs is couched in rather elementary category theory; I am not an expert in categories, but this work could not have been done without them. The theory sheds extra light on the calculi that can be expressed in it.

The lectures are based on a Tech Report written with Ole Jensen. You'll find pointers to this -- and other things, including the lecture slides -- on my web page www.cl.cam.ac.uk/users/rm135/. I shall begin with examples, including a beautiful one from Cardelli modelling biological membranes. Then I shall give the theory with some precision (but less pain than in the Tech Report), and show how to prove some non-trivial theorems about behaviour; they arose from joint work with Jamey Leifer. In particular, I'll show how Ole Jensen recovered exactly some theory of the asynchronous pi calculus. I shall finish by speculating what a programming language based upon bigraphical algebra might look like; with Danish colleagues I am hoping this may be some use in modelling and designing communications systems that are aware of physical locality.