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 is 13 March
  2. For those of you that did not attend the lectures: 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.
  3. The January '09 exam and solutions can be downloaded here

Course material

  1. Additional reading: Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. MIT Press, ISBN 0-262-03270-8
  2. More additional reading: Principles of Model Checking. Christel Baier and Joost-Pieter Katoen. MIT Press, ISBN 978-0-262-02649-9
  3. Handouts:
    1. week 2: Depth-First Search and Linear Graph Algorithms by R. Tarjan
    2. week 6: Bounded Model Checking by A. Biere, A. Cimatti, E. Clarke, O. Strichman, Y. Zhu
    3. week 8: Verification of Modal Properties Using Boolean Equation Systems by Angelika Mader
    4. week 11--12: Additional reading: Timed Automata by Rajeev Alur
    5. week 13--15: 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

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: Cancelled
  5. week 5: Symbolic Model checking: fairness and counterexamples (slides)
  6. week 6: Bounded Model Checking (slides)
  7. week 7: Mu-calculus (slides)
  8. week 8: Boolean Equation Systems (slides)
  9. week 9: Equivalences and Pre-orders: State Space Reduction and Preservation of Properties (slides)
  10. week 10: Data Abstraction (slides and example)
  11. week 11: Timed Verification: Timed Automata (slides)
  12. week 12: Timed Verification: Timed Automata (slides)
  13. week 13: Parameterised Boolean Equation Systems (slides)
  14. week 14: Cancelled due to illness. You can, however, test your skills on last year's exam
  15. week 15: Parameterised Boolean Equation Systems (slides)
For the '07-pages, see here. For the early years (< '07), see here.