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, mucalculus, etc) are studied and presented.
First day's announcements can be downloaded
here.
Important Notes:
 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.
 New this year: Parity Games, replacing data abstraction and
Bounded Model Checking
 No Timed Automata model checking this year;
 The January '09 exam and solutions can be downloaded here
Course material
 Additional reading (roughly covers the first 8 lectures):
Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled.
MIT Press, ISBN 0262032708
 More additional reading (roughly covers the first 5 lectures):
Principles of Model Checking. Christel Baier and JoostPieter Katoen.
MIT Press, ISBN 9780262026499
 Handouts and background material will be available for download here.
 week 2: DepthFirst Search and Linear Graph Algorithms by R. Tarjan
 week 8: Verification of
Modal Properties Using Boolean Equation Systems by Angelika Mader
 week 910: Optional reading:
 Parameterised
Boolean Equation Systems by J.F. Groote and T.A.C. Willemse
 Modelchecking Processes with Data by J.F. Groote and T.A.C. Willemse
 Static
Analysis Techniques for Parameterised Boolean Equation Systems by
S. Orzan, W.J. Wesselink and T.A.C. Willemse
 week 1115: Optional reading:
 An
experimental study of algorithms and optimisations for parity games,
with an application to Boolean Equation Systems by Jeroen Keiren

Recursive Solving of Parity Games requires Exponential Time by
Oliver Friedmann.

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