Algorithms for Model Checking (2IW55)

In these lectures, we study the model checking problem from an algorithmic viewpoint. In particular, algorithms for various temporal logics (CTL, LTL, mu-calculus, etc) are studied and presented.

First day's announcements can be downloaded here.

Important Notes:

  1. The next exam date is 29 January. The exam is open book, i.e., the book, handouts and slides may be used for consulting during the examination. Laptops, grannies and other auxiliaries are not allowed.
  2. New this year: Parity Games, replacing data abstraction and Bounded Model Checking
  3. No Timed Automata model checking this year;
  4. The January '09 exam and solutions can be downloaded here

Course material

  1. Additional reading (roughly covers the first 8 lectures): Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. MIT Press, ISBN 0-262-03270-8
  2. More additional reading (roughly covers the first 5 lectures): Principles of Model Checking. Christel Baier and Joost-Pieter Katoen. MIT Press, ISBN 978-0-262-02649-9
  3. Handouts and background material will be available for download here.
    1. week 2: Depth-First Search and Linear Graph Algorithms by R. Tarjan
    2. week 8: Verification of Modal Properties Using Boolean Equation Systems by Angelika Mader
    3. week 9--10: Optional reading:
      1. Parameterised Boolean Equation Systems by J.F. Groote and T.A.C. Willemse
      2. Model-checking Processes with Data by J.F. Groote and T.A.C. Willemse
      3. Static Analysis Techniques for Parameterised Boolean Equation Systems by S. Orzan, W.J. Wesselink and T.A.C. Willemse
    4. week 11--15: Optional reading:
      1. An experimental study of algorithms and optimisations for parity games, with an application to Boolean Equation Systems by Jeroen Keiren
      2. Recursive Solving of Parity Games requires Exponential Time by Oliver Friedmann.
      3. Small Progress Measures by M. Jurdzinski.

Course notes

  1. week 1: The temporal logics CTL*, CTL and LTL: syntax and semantics (slides)
  2. week 2: Fairness and Basic Model Checking Algorithms for CTL and fair CTL (slides)
  3. week 3: Symbolic Model Checking for CTL (slides)
  4. week 4: Symbolic Model checking: fairness and counterexamples (slides)
  5. week 5: Equivalences and Pre-orders: State Space Reduction and Preservation of Properties (slides)
  6. week 6: Exercises CTL*
  7. week 7: Mu-calculus (slides)
  8. week 8: Boolean Equation Systems (slides)
  9. week 9: Parameterised Boolean Equation Systems (slides)
  10. week 10: Parameterised Boolean Equation Systems (slides)
  11. week 11: Exercises (cancelled because of flu)
  12. week 12: Parity Games (slides)
  13. week 13: Parity Games (slides)
  14. week 14: Exercises mu-calculus
  15. week 15: Parity Games slides
  16. week 16: Questions/discussion
For the '07 and '08-pages, see here and here . For the early years (< '07), see here.