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.

Update

  1. Nov 13: Some typos have been fixed. Notable changes occurred in week 6 (fixed scoping of an if statement in the Emerson-Lei algorithm and corrected embedding of CTL into mu-calculus).
  2. Jan 3-4: Changed font settings as the previous font somehow did not print some characters such as [. Most changes in week 6 and week 15.
  3. Jan 5: Added exercises to weeks 11 and 12.
  4. Jan 21: 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 and grannies are not allowed.

Course material

  1. Required reading: Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. MIT Press, ISBN 0-262-03270-8
  2. Handouts:
    1. week 2: Depth-First Search and Linear Graph Algorithms by R. Tarjan
    2. week 5: Bounded Model Checking by A. Biere, A. Cimatti, E. Clarke, O. Strichman, Y. Zhu
    3. week 7: Verification of Modal Properties Using Boolean Equation Systems by A. Mader
    4. week 11--13: Optional reading: Timed Automata by R. Alur
    5. week 14--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: Symbolic Model checking: fairness and counterexamples (slides)
  5. week 5: Bounded Model Checking (slides)
  6. week 6: Mu-calculus (slides)
  7. week 7: Boolean Equation Systems (slides)
  8. week 8: Equivalences and Pre-orders: State Space Reduction and Preservation of Properties (slides)
  9. week 9: Data Abstraction (see slides for week 8 of previous year)
  10. week 10: Repetition of week 1-9, no new material
  11. week 11: Timed Verification: Timed Automata (slides)
  12. week 12: Timed Verification: Timed Automata (slides)
  13. week 13: Timed Verification: Timed Automata (slides)
  14. week 14: Parameterised Boolean Equation Systems (slides)
  15. week 15: Parameterised Boolean Equation Systems (slides)
For slides of previous years, see here. First day's announcements can be downloaded here.