2IW55 --- Algorithms for Model Checking (2010-2011)
In these lectures, we study the mu-calculus, CTL* and some of its subsets such as LTL and CTL, from a computational viewpoint. Among others, we treat the standard labelling algorithms and the symbolic (fixed point based) algorithms for CTL, and fair CTL. The Emerson-Lei algorithm for verifying the mu-calculus is analysed and its complexity is discussed. Transformations of the mu-calculus model checking problem to the frameworks of Boolean equation systems and Parity Games are addressed, combined with advanced algorithms for solving the latter artefacts. If time permits, reachability for real-time systems will be studied.
After
taking this course, students are expected
to
- be capable of explaining the computational complexity of the model checking algorithms for (fair) CTL and the modal mu-calculus
- be capable of transforming (fair) CTL formulae to the modal mu-calculus
- be able to explain the role of OBDDs in symbolic model checking
- be capable of simplifying Parity Games and parameterised Boolean equation systems
- be capable of explaining the computational complexity of the algorithms for solving Parity Games
- have the skills to manually execute the algorithms for model checking (fair) CTL, the modal mu-calculus, and reachability in a real-time setting
- be able to transform the problem of model checking to the modal mu-calculus to the problem of solving Boolean equation systems
- be able to transform the problem of solving Boolean equation systems to the problem of computing the winners in a Parity Game, and vice versa
- have the skills to manually solve (parameterised) Boolean equation systems and Parity Games using the algorithms presented in the course.
Important Notes
- Lectures are Friday morning, 8.45 -- 10.30 in L10, Pav.
- Note: first lecture is 10 September. An extra lecture is scheduled for 10.45 -- 12.30, Wednesday 12 January, 2011 in Aud. 15.
- The next exam date is 14.00 -- 17.00, Thursday 20 January, 2011. 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.
Course material
- Additional reading (roughly covers the first 7 lectures): Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. MIT Press, ISBN 0-262-03270-8.
- 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.
Handouts, background material and announcements will be made available for download below:
- week 1: domestic announcements can be downloaded here
- week 2: Depth-First Search and Linear Graph Algorithms by R. Tarjan
- week 8: Verification of Modal Properties Using Boolean Equation Systems by Angelika Mader
- week 9--10:
Optional reading:
- Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems by B. Ploeger, W.J. Wesselink and T.A.C. Willemse
- Model-checking 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 11--13: Optional reading:
Topics and course notes
Part 1:
- 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 Pre-orders: State Space Reduction and Preservation of Properties (slides)
- week 6: Mu-calculus (slides)
- week 7:
Exercises
Additional
exercises
for Part 1 can be downloaded here.
- week8: Boolean Equation Systems (slides). Example BES files for experimenting, the grammar and their (partial) solutions are contained in the following archive: here
- week 9: Parameterised Boolean Equation Systems (slides)
- week 10: Parameterised Boolean Equation Systems (slides)
- week 11: Parity Games (slides; update: minor bug fixes and additions). Lecturer: Jeroen Keiren
- week 12: Parity Games (slides). Lecturer: Jeroen Keiren
- week 13: Parity Games (slides). Lecturer: Jeroen Keiren
- week 14 (1): Exercises. Lecture room AUD 15, 10:45-12:30, Wednesday 12 January
- week 14 (2): Wrap-up/Outlook (slides)
Looking
to see how you fared on the January exam? (exam, solution)
Some
statistics on the grades for the questions in the exam
itself:
1a | 1b | 2a | 2b | 3a | 3b | 3c | 4a | 4b | |
mean | 12 | 10 | 9 | 6 | 4 | 3 | 5 | 9 | 14 |
stdev | 4.9 | 3.5 | 1.8 | 4.0 | 2.3 | 2.0 | 4.8 | 3.3 | 6.5 |
min/max | 0/15 | 4/15 | 4/10 | 0/10 | 0/5 | 0/5 | 0/10 | 0/10 | 3/20 |