Course pages 2019–20

# Topics in Concurrency

**Principal lecturer:** Prof Glynn Winskel**Taken by:** MPhil ACS, Part III**Code:** L301**Hours:** 16**Prerequisites:** Semantics of programming languages, specifically, an idea of operational semantics and how to reason from it.

## Aims

The aim of this course is to introduce fundamental concepts and techniques in the theory of concurrent processes. It will provide languages, models, logics and methods to formalise and reason about concurrent systems. Students will be assessed by a one-hour test at the end of the course.

## Lectures

**Simple parallelism and nondeterminism**. Dijkstra’s guarded commands. Communication by shared variables: A language of parallel commands. [1 lecture]**Communicating processes**. Milner’s Calculus of Communicating Processes (CCS). Pure CCS. Labelled-transition-system semantics. Bisimulation equivalence. Equational consequences and examples. [3 lectures]**Specification and model-checking**. The modal mu-calculus. Its relation with Temporal Logic, CTL. Model checking the modal mu-calculus. Bisimulation checking. Examples. [3 lectures]**Introduction to Petri nets**. Petri nets, basic definitions and concepts. Petri-net semantics of CCS. [1 lecture]**Cryptographic protocols**. Cryptographic protocols informally. A language for cryptographic protocols. Its Petri-net semantics. Properties of cryptographic protocols: secrecy, authentication. Examples with proofs of correctness. [2 lectures]**Event structures**. Their relation with Petri nets and representation via rigid families. The CCS operations on event stuctures. Maps of event structures. [2 lectures]**Games and strategies as event structures**, an introduction to Concurrent Games. Composing strategies - interaction and hiding. A special case: nondeterministic dataflow. [2 lectures]**Strategies as concurrent processes**. A higher-order language for strategies. May and must equivalence. Probabilistic and quantum strategies briefly. The future? [2 lectures]

## Objectives

At the end of the course students should

- know the basic theory of concurrent processes: non-deterministic and parallel commands, the process language CCS, its transition-system semantics, bisimulation, the modal mu-calculus, Petri nets, event structures, a language and reasoning techniques for cryptographic protocols, and the basics of concurrent games;
- be able to formalise and to some extent analyse concurrent processes: establish bisimulation or its absence in simple cases, express and establish simple properties of transition systems in the modal mu-calculus, argue with respect to a process language semantics for secrecy or authentication properties of a small cryptographic protocol, apply the basics of concurrent games.

## Recommended reading

Comprehensive notes will be provided.

Further reading:

* Aceto, L., et. al. (2007). *Reactive systems: modelling, specification
and verification*. Cambridge University Press.

Milner, R. (1989). *Communication and concurrency*. Prentice Hall.

Milner, R. (1999). *Communicating and mobile systems: the Pi-calculus*.
Cambridge University Press.

Winskel, G. (1993). *The formal semantics of programming languages, an
introduction*. MIT Press.

Winskel, G. (2011-) “The ECSYM notes: Event structures, stable families and
games”. Notes for the ERC Research project *Events, Causality and Symmetry
(ECSYM)*. Available at: `https://www.cl.cam.ac.uk/ gw104/ecsym-notes.pdf`

## Further Information

Current Cambridge undergraduate students who are continuing onto Part III or the MPhil in Advanced Computer Science may only take this module if they did NOT take it as a Unit of Assessment in Part II.

## Assessment

Written test

This course is borrowed from Part II of the Computer Science Tripos. As such, assessment will be adjusted to an appropriate level for those enrolled for Part III of the Tripos or the M.Phil in Advanced Computer Science. Further information about assessment and practicals will follow at the first lecture.