Course pages 2013–14
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
Aims
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.
Syllabus
- 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]
Objectives
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.
Assessment
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.