Tentative Schedule

Week 1 [draft notes]
  • Overview of the course (Daniel and Damien)
  • Reminder about basic automata theoretic concepts (Daniel)
Week 2 [draft notes] (Damien)
  • Petri Nets
  • Verification using linear programming
Week 3 [draft notes] (Damien and Ivan)
  • Structural properties: siphons, traps
  • Boundedness
  • Karp and Miller Tree
Week 4 [draft notes] (Ivan and Daniel)
  • Well-Structured Transition Systems
  • Backward coverability algorithm
Week 5 [draft notes] (Damien)
  • 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] (Daniel)
  • Communicating state machines
  • Turing completeness of communicating state machines with reliable FIFO channels
Week 7 [draft notes] (Damien)
  • Lossy Channel System
  • Simple regular expression and WQO for LCS
Week 8 [draft notes] (Damien)
  • LTS, Simulations and bisimulations
  • Calculus of Communicating Systems (CCS)
  • Structural congruence
  • Expressive power of CCS
Week 9 [draft notes] (Damien)
  • Weak (bi-) simulation
  • The π‑calculus
Week 10 [draft notes] (Damien)
  • Variations and extensions of the π-calculus
  • Typing communicating processes
Week 11 [draft notes] (Damien)
  • Bulk synchronous model
  • Analysis of bulk synchronous programs and cut-off bound
Week 12 [draft notes] (Damien)
  • Weak memory model
  • TSO (Total Store Order)
  • WSTS for TSO
Week 13 (Damien)
  • Recap and Context
  • Q&A for Theory
Week 14 (Damien)
  • Q&A for Theory and Exercises



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