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

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.

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

Category theory

Game Semantics

Evaluation

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