Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Lecture: Concurrency Theory

Winter term 2019/20


October 2
The first lecture will take place on Monday, October 28, at 09:45 in room IZ 358.


Lecture Notes

Lecture notes (last updated on March 25, 2018)

There are also handwritten notes on some chapters of the lecture:

Furthermore, there is material by Roland Meyer from past iterations of the lecture:


The exercise sheets will be made available here. Please hand in your solution in groups of 2 to 3 people in the box next to room 343 in the Institute for Theoretical Computer Science, Muehlenpfordtstr. 23. If you have questions or encounter problems with the exercises, please contact Prakash or Peter.


Sucessfully finishing the module consists of two parts:


The topic of the lecture is the verification of concurrent systems. We will study automata models for these systems (e.g Petri nets, WSTS, and distributed automata) and show how algorithmic problems for these models can be solved.

We plan to cover the following topics in detail:

  • Petri nets: Reachability and coverability
  • Well-structured transition systems
  • Distributed automata
  • Multi-pushdown automata
  • TSO - A weak memory model for x86


The following is the list of contents occording to the Modulhandbuch. The topics that we will cover in the lecture are a subset, see the description above.


The lectures will be based upon the following books and articles. Most of them are available online, the remaining ones can be found in the library.