Week 1 [lecture notes]
  • Overview of the course
  • Reminder about basic automata theoretic concepts
Week 2 [lecture notes]
  • Petri Nets
  • Verification using linear programming
Week 3 [lecture notes]
  • Structural properties: siphons, traps
  • Boundedness
  • Karp and Miller Tree
Week 4 [lecture notes]
  • Well-Structured Transition Systems
  • Backward coverability algorithm
Week 5 [lecture notes]
  • Ideal Completion for WSTS
  • Forward coverability algorithm
Week 6 by Marko Horvat [slides]
  • Modeling and verification of security protocols
Week 7 [lecture notes]
  • Communicating state machines
  • Turing completeness of communicating state machines with reliable FIFO channels
Week 8 [lecture notes]
  • Lossy Channel System
  • Simple regular expression and WQO for LCS
  • LTS, Simulations and bisimulations
Week 9 [lecture notes]
  • CCS
  • Structural congruence
  • Algebraic laws of bisimulation
  • Decidability of bisimulation
Week 10 [draft lecture notes]
  • The π‑calculus
  • Communication Topologies and Mobility
  • Graphical interpretation of the π‑calculus
Week 11 [draft lecture notes]
  • Term embedding and the notion of depth
  • The WQO of processes with depth at most k
  • Coverability for depth-bounded processes
Week 12 [draft lecture notes]
  • Further analysis on depth-bounded processes
  • Variations and extensions of the π-calculus
  • Typing communicating processes
Week 13 [draft lecture notes]
  • Bulk synchronous model and cut-off bound
  • Q&A
Week 14
  • Recap
  • Q&A



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