## 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.