Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory
Computer Science Syllabus - Topics in Concurrency
Computer Laboratory > Computer Science Syllabus - Topics in Concurrency

Topics in Concurrency next up previous contents
Next: VLSI Design Up: Lent Term 2006: Part Previous: Quantum Computing   Contents

Topics in Concurrency

Lecturer: Professor G. Winskel

No. of lectures: 12 lectures

Prerequisite course: Semantics of Programming Languages (specifically, an idea of operational semantics and how to reason from it)


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.


  • Simple parallelism and nondeterminism. Dijkstra's guarded commands. Communication by shared variables: A language of parallel commands.

  • Communicating processes. Milner's Calculus of Communicating Processes (CCS). Pure CCS. Labelled-transition-system semantics. Bisimulation equivalence. Equational consequences and examples.

  • Specification and model-checking. The modal mu-calculus. Its relation with Temporal Logic, CTL. Model checking the modal mu-calculus. Bisimulation checking. Examples.

  • Introduction to Petri nets. Petri nets, basic definitions and concepts. Petri-net semantics of CCS.

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

  • Mobile computation. An introduction to process languages with process passing and name generation. The Pi-Calculus and Ambient Calculus briefly.


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, languages for cryptographic protocols and mobile computation.

  • 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, formalise mobile computation.

Recommended reading

Comprehensive notes will be provided.

Further reading:

* 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.
Milner, R. (1989). Communication and concurrency. Prentice-Hall.

next up previous contents
Next: VLSI Design Up: Lent Term 2006: Part Previous: Quantum Computing   Contents
Christine Northeast
Sun Sep 11 15:46:50 BST 2005