Tentative Schedule

Week 1 [draft notes]
  • Overview of the course [notes]
  • Reminder about basic automata theoretic concepts
Week 2 [draft notes]
  • Properties and Verification
  • Petri Nets
  • Verification using linear programming
Week 3 [draft notes]
  • Termination and Boundedness
  • Karp and Miller Tree
  • "Size" of Bounded Petri Nets
Week 4 [draft notes]
  • Well-Structured Transition Systems
  • Backward coverability algorithm
Week 5 [draft notes]
  • Forward coverability algorithm (The notes have quite a lot of material. We will trim them down depending on what we have the time to cover in class.)
Week 6 [draft notes]
  • Communicating state machines
  • Turing completeness of communicating state machines with reliable FIFO channels
Week 7 [draft notes]
  • Lossy Channel System
  • Simple regular expression and WQO for LCS
Week 8 [draft notes]
  • LTS, Simulations and bisimulations
  • Calculus of Communicating Systems (CCS)
  • Structural congruence
  • Expressive power of CCS
Week 9 [draft notes]
  • Weak (bi-) simulation
  • The π‑calculus
  • Variations and extensions of the π-calculus
Week 10
Week 11
Week 12 [draft notes]
  • Weak memory model
  • TSO (Total Store Order)
  • WSTS for TSO
Week 13
Week 14
  • Q&A for Theory and Exercises


You can see that we are about to compile master solutions for the exercises. However, due to resource constraints, we will probably not be able to cover all of them until the first exams. This is why we encourage you to send an e-mail to Damien and Felix if you liked to have a particular solution. This way, we can prioritise accordingly. In case, we will not manage to write them up in time, we would like to hint at the office hour on Monday 2nd of March again.


Creative Commons License
The files available in are licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.