Mathematical models of concurrent or distributed systems typically belong to one of two families: interleaving models, which represent a concurrent system by enumerating its exponentially many schedulings, and independence models, which instead represent explicitly information of causality or independence between computational events. They address the need for an abstract representation for the behaviour of concurrent or distributed systems, to be used for various purposes, from the semantic study and the design of concurrent programming languages to the formal verification of distributed systems. This course focuses on independence or causal models of concurrency, which are more precise and mathematically elaborate than their interleaving counterparts. The course will introduce various notions of interleaving (transition systems) and independence (Petri nets, Mazurkiewicz trace languages, event structures) models, along with tools for reasoning on them (bisimulation and open maps) and comparisons between them.
The course will then give an introduction to ongoing research in developing a mathematical theory of distributed (or concurrent) games. Games and strategies are very commonly used in logic and computer science (among many other fields), typically to model interactive or open systems. But games considered in the literature often have a very restricted structure: they are sequential, and the players often have to alternate. In contrast the games presented here, based on event structures, allow a Player (or a team of players) to interact and compete against an Opponent (or a team of opponents) in a highly distributed fashion, with no recourse to interleavings. We will illustrate the model by an application to the semantics of a simple concurrent programming language.
All these developments rely on some notions of category theory which we will introduce along the way.
You can find additional material on CCS and Petri nets in the Cambridge lecture notes ``Topics in Concurrency'' here.
Categories, functors, natural transformations: Chapter 1 of Tom Leinster's book.
Products, equalizers, pullbacks: Section 5.1 of Tom Leinster's book (p.107-117).
Dual category, product category: section 1.1 of the book.
Subcategories, full and faithful functors, presheaves, covariance/contravariance: section 1.2 of the book.
Natural isomorphisms, equivalence of categories: section 1.3 of the book.
Adjunctions via natural bijections: section 2.1 of the book.
Main evaluation will be a final exam.
Additional evaluation (leading to bonus on the final grade) will be based on homework (probably every two weeks).