This advanced course addresses Bachelor and Master students in Computer Science. Background in concurrency theory is of advantage but not mandatory.


The aim of this course is to provide students with basic principles and concepts underlying a correct concurrent programming with or without code mobility.

This is achieved considering algebraic models, that is, simple languages that provide all basic features of real concurrent languages.

These models, commonly named process calculi (such as CCS, pi-calculus, Mobile Ambient), being simpler than real languages, are well suited to the study in a formal way typical problems of concurrency.

During the course there will be proposed examples of systems modeled as processes as well as of mobile agents.

Overview of the course

Remarks on CCS: syntax, operational semantics, strong/weak bisimulation
Checking bisimilarity: bisimulations as games and decision algorithms
Property specification and verification: Hennessy-Milner Logic
Mobile systems
pi-calculus: syntax and operational semantics
Examples of mobile systems in pi-calculus
Strong and weak bisimulation for pi-calculus
Concurrent and distributed models
Mobile ambients
Probability extension: CCSp
Security extension: Spi-calculus

Reference books

Main book:

- R. Milner, "Communicating and Mobile Systems: the pi calculus", Cambrigde University Press, 1999.


Auxiliar book for the first part of the course:

- L. Aceto et al., "Reactive Systems: Modelling, Specification, and Verification". A draft of this book is available as online PDF.

Time and location

The course spans over the summer term 2012.


Lectures take place Mon 12:00-14:00 in E1.3, HS 001.


Tutorials and exercise meetings, when given, take place Fri 08:15-10:00 in E1.3, SR 016.

Exam schedule

Mid-term exam: June 11th at 12:00-14:00 in E1.3, HS 001


Final exam: August 3rd at 09:00-11:30 in E1.3, HS 001


Re-exam: August 28th at 10:00-12:30 in E1.3, HS 001


If you would like to participate in this course, please register for it via the CMS. An explanation how to do that is here (requires Adobe Flash Player).


Dr. Andrea Turrini