Computer Laboratory
Gian Luca Cattani and I have worked on a path-based domain theory for interacting processes, one aim being a general theory of bisimulation, also for higher-order process languages. This mini-course will explain the origins of this work and the ideas and mathematics on which it rests.
The first lecture should be very accessible and give a gentle introduction to the advantages of viewing models for concurrency as categories, in which the arrows are forms of simulation. It will show how many operations of process algebra arise as universal constructions in a category and introduce a general definition of bisimulation based on ``open maps''. The lecture will be mainly based on the familiar model of labelled transition systems, but will indicate how the ideas are equally applicable to other models such as event structures and Petri nets, and how relations between different models are often expressed as adjunctions.
The following lectures will introduce and motivate a broader space of models of concurrent computation, leading to a form of domain theory for concurrency, in which nondeterministic processes are represented by presheaves; the role of domain will be replaced by that of presheaf category. There are several ways to introduce presheaves, but this course will emphasise the guiding intuition that presheaves are a form of transition system which allow computation paths to have a variety of forms. Bisimulation between presheaves is again obtained from open maps. Here a useful theorem is that colimit-preserving functors between presheaf categories preserve open maps, and so bisimulation. Its proof will be presented, helped some of the way by the view of presheaves as transition systems.
Finally, I hope to give an idea of the languages for concurrency and the concepts of linearity and nonlinearity the mathematics suggests.