Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Lecture: Concurrency theory

Winter term 2018/19


December 2
There will be no lecture on Wednesday, December 5.
October 5
The first lecture will take place on Tuesday, October 16 October 23, at 11:30 in room IZ 358.


Lecture Notes

Lecture notes (last updated on March 25, 2018)

If you have questions or spot a bug in the notes, please contact Elisabeth.

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 Elisabeth.


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.