Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Lecture: Concurrency theory

Winter term 2017/18


January 24
We will give some overview over the material that is relevant for the oral exam during the final exercise class on Wednesday, January 31.
January 24
The final exercise sheet and the updated lecture notes are now available.
January 19
We have updated Exercise sheet 11, clarifying the meaning of the program in Exercise 2. (The program itself remains unchanged.)
January 16
Information on the oral exams can be found below.
January 10
The new exercise sheet is available! We will add the material on TSO to the lecture notes later.
December 21
The new exercise sheet is available! We wish all of you a Merry Christmas and a happy New Year!
December 13
The lecture and exercise classes for today are canceled!
November 09
Exercise-4, question 1c should read do you need labels on the edges. Also note that there is a modification to the question 2a.
October 20
There was a minor bug in the definition of the Ackermann function in Exercise 3 that we just have fixed.
October 18
The first exercise sheet and the lecture notes are now available.
October 9
The first lecture will take place on Tuesday, October 17, at 11:30 in room IZ 358.

Oral exams


Lecture Notes

We offer lecture notes that will be updated during the term.

Lecture notes (last updated on February 2)

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

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 Sebastian or Prakash.


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.

Traditionally, the contents of this lecture change every year. True to this spirit, the syllabus of this year's lecture will overlap, but not be same, as the one of the past four iterations of the lecture.

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

You can find more details on these topics in the introduction of the lecture notes (to be uploaded soon).


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.