Computer Laboratory

Course pages 2012–13

Advanced Topics in Concurrency

Principal lecturer: Prof Glynn Winskel
Taken by: MPhil ACS, Part III
Code: L22
Hours: 8
Prerequisites: Category theory course such as Category Theory and Logic L108 module


This module gives a rapid introduction to the major models for concurrent computation, especially "causal" or "independence" models such as Petri nets and event structures which are becoming increasingly important in today's semantics and verification, and how they are related and used in the semantics and verification of concurrent/distributed computation from the verification of security protocols, to game semantics and systems biology.


  • Models for concurrency: transition systems, Petri nets, Mazurkiewicz trace languages, interleaving versus independence models [2 lectures]
  • Bisimulation and open maps [2 lectures]
  • Event structures and stable families [2 lectures]
  • Graph rewriting and rule-based systems biology [2 lectures]


On completion of this module, students should:

  • know about transition systems, Petri nets, Mazurkiewicz trace languages, event structures and how they are related;
  • be able to apply such models to semantics and basic reasoning;
  • have insight into their use over a variety of areas, especially in rule-based systems biology.


By take-home test.

Recommended reading

Notes and articles will be provided. They will probably include:

Winskel, G. & Nielsen, M. (1993). Models for concurrency. A chapter in the Handbook of Logic in Computer Science. Oxford University Press.
Joyal, A., Nielsen, M. & Winskel, G. (1996). Bisimulation from open maps. An article in Information and Computation.