Models of concurrency, categories, and games
Description
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.
Teachers
Lectures
- Lecture 1 (Glynn, 13/09/17). General motivations (domains,
semantics). CCS, Petri nets. Here are the slides.
You can find additional material on CCS and Petri nets in the Cambridge lecture notes ``Topics in
Concurrency'' here.
- Lecture 2 (Pierre, 20/09/17). Basic categories. Universal properties,
categories, cartesian categories, coproducts, equalizers, pullbacks, functors, natural
transformations.
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).
- Lecture 3 (Glynn, 27/09/17). Event structures, stable families, maps
between those. Here are the slides.
- Lecture 4 (Pierre, 04/10/17). Subcategories, full and faithful
functors, functor categories, presheaves, natural isomorphisms, equivalence of categories, dual
category, covariance and contravariance, product category, bifunctors, adjunctions via natural
bijection.
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.
- Lecture 5 (Glynn, 11/10/17). Adjunction between event structures and
stable families. Same slides.
- Lecture 6 (Pierre, 25/10/17). Vertical/horizontal composition of
natural transformations. Adjunctions via unit and co-unit. Examples of units and co-units. Products
as representations, right adjoints preserve products.
Horizontal composition of natural transformations, interchange law: p.37-38 of the book.
Adjunctions via unit and co-unit: section 2.2 of the book.
- Lecture 7 (Glynn, 08/11/17). Constructions in stable families and
event structures. Products, restrictions, pullbacks. Here are the slides, and
the course notes.
- Lecture 8 (Pierre, 15/11/17). Overview of denotational semantics,
motivations for denotational semantics of concurrent programming languages. Reminder of the
lambda-calculus. Adjunctions via cofree objects. Cartesian closed category. Syntactic cartesian
closed category, interpretation of the lambda-calculus in a cartesian closed category. Soundness and
completeness of the interpretation.
Cartesian closed categories are covered very briefly in the book
(p.165-168), without the connection to the lambda-calculus.
The reference for the correspondence between cartesian closed categories and the lambda-calculus is the book
"Introduction to higher-order categorical logic" by Lambek and Scott, which is not available online. The content of the
lecture can also be found (with slightly different notational conventions) in Streicher's notes on categorical logic (p.61-76).
- Lecture 9 (Glynn, 22/11/17). Concurrent strategies. Interaction of
concurrent strategies, composition, copycat strategy. Here are the slides and course notes.
- Lecture 10 (Glynn, 29/11/17). Deterministic strategies. slides and course notes.
- Lecture 11 (Pierre, 13/12/17). Monoidal categories, symmetric
monoidal categories, compact closed categories, symmetric monoidal closed categories. The compact
closed category of concurrent strategies.
Homework
Summary of contents (subject to change)
Note: the order is not as given here, as courses on concurrency and category theory will be
interleaved.
- Models of concurrency (Glynn Winskel)
- General motivations: domains, semantics
- CCS, transition systems, Petri nets
- Stable families, event structures, unfoldings
- Event structure model of CCS
- Category theory (Pierre Clairambault)
- Categories, functors, natural transformations
- Adjunctions, limits
- Symmetric monoidal categories and the affine lambda-calculus
- Compact closed categories, bicategories (?)
- Concurrent games (Pierre Clairambault and Glynn Winskel)
- Games, strategies, composition
- Compact closed structure (and the linear lambda-calculus)
- Concurrent game semantics of programming languages
- Extensions: probabilities, ...
Prerequisites
Some familiarity with labeled transition systems and the lambda-calculus would help (typically, the
M1 courses "Semantics and Verification" and "Programs and Proofs").
References
Models of concurrency
- Glynn Winskel and Mogens Nielsen. Models for concurrency, a chapter in the Handbook of Logic
in Computer Science (1993). Oxford University Press.
- Glynn Winskel, Notes for Topics in Concurrency, a Part II Computer Science course at the University of
Cambridge, [lecture notes]
Category theory
- Tom Leinster Basic Category Theory, 2016. [book]
Game Semantics
- Samson Abramsky, Guy McCusker, Game Semantics, 1998. [book chapter]
- Glynn Winskel, Notes for Advanced Topics in Concurrency: Concurrent games, a Part III and
MPhil Computer Science course at the University of Cambridge, 2014. [lecture notes]
Evaluation
Main evaluation will be a final exam.
Additional evaluation (leading to bonus on the final grade) will be based on
homework.