Course pages 2013–14
Advanced Topics in Concurrency
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.
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.