Concurrency Theory


  • 30.01.2018: The times & dates of the oral exams have been sent around via Campus Mail. Since the exam will take place either in Prof. Nolls or Prof. Katoens office, be at the chair/secretaries office shortly before your scheduled time to be picked up.
  • 18.12.2017: During the first lectures you have been informed that admission to the Concurrency Theory exam requires a certain percentage of points to be obtained in the exercises. However, this requirement is not fixed in the corresponding module specification and thus invalid. For this reason, every registered participant is automatically admitted. Therefore, if you are not intending to attend the exam please de-register via Campus Office in order to avoid a “not passed” due to not showing up. Although the exercises are no longer mandatory for the exam admission, we will continue to correct them and discuss them in the exercise classes. We firmly believe that actively solving the exercises is truly important so as to pass the exam.
  • 11.12.2017: Exercise 8, clarification: State “t” in Ex8.2 should be t_4, the topmost state in the transition system.
  • 24.10.2017: Exercise 2, clarification: A label denotes a particular state in the labelled transition system.
  • 16.10.2017: Please find here  an electronic version of the information concerning the questionnaire about the effect of supplementary study material in digital form on studying concurrency theory as carried out at the TU Berlin. We recommended to participate!
  • 2017-09-18: We are online!


Type Day Time Hall Start Lecturer
Lecture Mon 14:15 – 15:45 9U10 09 Oct Katoen/Noll
  Thu 14:15 – 15:45 9U10 12 Oct Katoen/Noll
Exercise Fri 14:15 – 15:45 9U10 20 Oct Berger/Junges


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 Lecturer Topic Slides Handout
1 09 Oct Noll Introduction l1 l1 
2 12 Oct Noll Calculus of Communicating Systems (CCS) l2 l2
3 16 Oct Katoen Hennessy-Milner Logic l3 l3
4 23 Oct Noll Hennessy-Milner Logic with Recursion l4 l4 
5 26 Oct Noll Fixed-Point Theory l5 l5
6 02 Nov Katoen Mutually Recursive Equational Systems l6  l6
7 06 Nov Noll Modelling and Analysing Mutual Exclusion Algorithms & Value-Passing CCS l7 l7 
8 09 Nov Noll The π-Calculus l8 l8
9 13 Nov Noll Variations of π-Calculus l9 l9
10 16 Nov Noll Trace Equivalence l10 l10
11 20 Nov Noll Strong Bisimulation l11  l11
12 23 Nov Katoen Strong Bisimulation Properties l12   
13 27 Nov Katoen Bisimulation Games and Fixed Points l13   
14 30 Nov Katoen Weak Bisimulation l15 l15
15 04 Dec Katoen Strong Bisimulation and HML  l16   l16
16 11 Dec Noll Interleaving Semantics of Petri Nets l17  l17 
17 14 Dec Katoen True Concurrency Semantics of Petri Nets (I) l18 l18 
18 18 Dec Katoen Branching Processes l19  l19 
19 08 Jan Katoen McMillan Prefixes l20  l20
20 15 Jan Katoen Petri Net Semantics of CCS    


No. Due Date Topic Exercise Solution
1 20 Oct CCS  exercise01 solution01 
2 27 Oct HML exercise02  
3 03 Nov Recursive HML, Complete Lattices exercise03 see L2p
4 10 Nov Mutually Recursive Equation Systems exercise04 see L2p
5 17 Nov Value-Passing, HML, Pi Calculus exercise05 see L2p
6 24 Nov Pi Calculus, Recursive Definitions  exercise06   
7 8 Dec Trace Equivalence, Bisimulation exercise07  
8 15 Dec Weak Bisimulation exercise08  
9 12 Jan Characterising HML, Interleaving Petri Nets exercise09  
10 19 Jan Petri Nets, Distributed Runs exercise10  


  • There will be an oral exam. Possible dates will be announced later.
  • Registration is possible via this web page.
  • Admission requires to achieve 50% of the points in the exercises.

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.