Next: Easter Term 2001: Part
Up: Lent Term 2001: Part
Previous: Security
Lecturer: Professor G. Winskel
(gw104@cl.cam.ac.uk)
No. of lectures: 12
Prerequisite courses: Semantics of Programming Languages
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.
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.
Model checking the modal mu-calculus. Bisimulation checking.
The Concurrency Workbench. 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 transition-system semantics. Its
Petri-net semantics. Properties of cryptographic protocols: secrecy,
authentication. Examples with proofs of correctness. [3 lectures]
- Mobile computation.
A quick introduction to process languages with name generation and
process passing. The Pi-Calculus and Ambient Calculus. [1 lecture]
Objectives
At the end of the course students should
- know the basic theory of concurrent processes:
nondeterministic and parallel commands, the process language CCS, its
transition-system semantics, bisimulation, the modal mu-calculus,
Petri nets, the Concurrency Workbench, a process language for
cryptographic protocols
- 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
Recommended books
Comprehensive notes will be provided.
Further reading:
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.
Next: Easter Term 2001: Part
Up: Lent Term 2001: Part
Previous: Security
Christine Northeast
Wed Sep 20 15:13:44 BST 2000