Concurrency Theory


  • 2016-03-01: We are glad to announce that everybody who participated in the first exam did so successfully! In case the official exam inspection date is not convenient for you (or in case you cannot wait to know your grade), you may also drop by earlier and see whether we have time for an individual exam inspection.
  • 2016-02-26: The announcement of the grades and the inspection of the first exam takes place Thursday, March 3, from 14:00h to 16:00h in our seminar room (Room 4201b).
  • 2016-02-10: Please find two old exams in section “Exam”.
  • 2016-02-01: There will be a Q&A session on Monday, February 22 at 14:00h in Room 5055. Nota bene: Your questions are more likely to be answered satisfactorily if you send us your questions a few days in advance. Notice furthermore that there will be no excercise nor lecture on February 8 and that the final lecture was shifted to Wednesday, February 10 at 10:15h in Room 5052.
  • 2016-01-15: The lecture on February 11 is shifted to Wednesday, February 10 at 10:15 and will be held in seminar room 5052.
  • 2015-12-21: Due to a shortage of larger lecture halls, the next exercise class on January 11 will take place in our seminar room (room 4201b).
  • 2015-11-20: We corrected two typos in the second task of exercise sheet 3. We are sorry for the inconvenience.
  • 2015-10-27: Please note that exercise sheet 1 has changed in order to be compliant with the material presented in the lecture so far. 
  • 2015-09-08: We are online!


Type Day Time Hall Start Lecturer
Lecture Mon 14:15 – 15:45 AH 1 19 Oct Katoen/Noll
Thu 14:15 – 15:45 AH 2 12 Nov Katoen/Noll
Exercise Mon 10:15 – 11:45 AH 6 26 Oct Kaminski/Matheja


Today, concurrent programming has become mainstream, dictated by need for ever increasing performance which, having reached the end of Moore’s law, can only be achieved by parallelism. Indeed, application software from areas such as medicine or natural sciences heavily relies on parallel hardware infrastructure like (GP)GPU accelerators, FPGAs, and multi- and many-core machines.
However, it is also today that we see concurrency faults coming up every day. The simple reason is that writing concurrent programs is difficult. Most programmers “think sequentially” and therefore make mistakes when writing concurrent software. Notorious programming errors include deadlock and violations of atomicity or order of operations, which are mainly caused by the wrong use of synchronization primitives like semaphores or locks. Even worse, the inherent non-deterministic behavior of concurrent software makes bugs difficult to reproduce. Addressing these challenges requires efforts from multiple related disciplines, involving concurrency bug detection, program testing and validation, and programming language design.
Another important area of computer science where concurrency naturally arises is that of reactive systems, which maintain an ongoing interaction with their environment. In contrast to sequential systems whose meaning is defined by the results of finite computations, the behavior of reactive systems is mainly determined by concurrent execution, communication, interaction, and mobility of non-terminating processes. Typical examples include operating systems, control systems for production lines, power plants, or vehicles. As many of such systems are safety critical, their development calls for rigorous formal techniques for design, implementation, and validation.
The aim of this course is to provide a basic understanding of modeling formalisms for concurrent systems. It will address two basic approaches, which are respectively called the interleaving and the true concurrency approach. The former is based on the idea to reduce the phenomenon of concurrency to well-known concepts, by interpreting parallel behavior as non-deterministic merging of sequential execution. It is represented by various process algebras, which provide a formal apparatus for reasoning about structure and behavior of systems in a compositional way. The true concurrency approach mainly comes in the form of Petri nets, which are well suited for explicitly modeling the concurrent behavior of distributed systems.


Basic knowledge of the following relevant undergraduate courses is expected:
  • Programming (essential concepts of imperative and object-oriented programming languages and elementary programming techniques)
  • Essential concepts of operating systems
  • Formal Languages and Automata Theory (regular and context-free languages, finite and pushdown automata)
  • Mathematical Logic


No. Date Topic Slides Handout Exercise Solution
1 19 Oct Introduction l1 l1
2 26 Oct Calculus of Communicating Systems (CCS) l2 l2 e1 s1
3 09 Nov Hennessy-Milner Logic l3 l3 e2 s2
4 12 Nov Hennessy-Milner Logic with Recursion l4 l4
5 16 Nov Fixed-Point Theory l5 l5 e3 s3
6 19 Nov Mutually Recursive Equational Systems l6 l6
7 23 Nov Modelling and Analysing Mutual Exclusion Algorithms l7 l7 e4 s4
8 26 Nov Extensions and CCS: Value Passing and Mobility l8 l8
9 30 Nov The π-Calculus l9 l9 e5 s5
10 07 Dec Variations of π-Calculus l10 l10  e6 s6
11 10 Dec Trace Equivalence l11 l11  e7 s7
12 17 Dec Strong Bisimulation l12 l12
13 11 Jan Bisimulation Games l13 l13 e8 s8
14 14 Jan Weak Bisimulation l14 l14
15 18 Jan HML and Strong Bisimulation l15 l15 e9 s9
16 21 Jan Interleaving Semantics of Petri Nets l16 l16  e10 s10
25 Jan Introduction to CAAL Tool
17 28 Jan True Concurrency Semantics of Petri Nets I  l17  l17
18 Wed 10 Feb 10:15 (Room 5052) True Concurrency Semantics of Petri Nets II l18  l18
Mon 22 Feb 14:00 (Room 5055) Q&A Session


  • The first and second written exam are respectively scheduled for Friday, February 26, 11:30 at AH 2 and Tuesday, March 29, 10:00 at AH 1.
  • Two old exams can be found here and here.

Evaluation results

Further information

  • The lectures will be given in German or English, depending on the language proficiency of the audience.
  • The slides and other course material will be in English. There are no lecture notes (yet); the course material will consist of slides.

Background Literature

  • Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen and Jiri Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
  • Wolfgang Reisig: Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Springer Verlag, 2012.
  • Maurice Herlihy and Nir Shavit: The Art of Multiprocessor Programming. Elsevier, 2008.
  • Jan Bergstra, Alban Ponse and Scott Smolka (Eds.): Handbook of Process Algebra. Elsevier, 2001.