2IW55 --- Algorithms for Model Checking
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 symbolic (fixed point based) algorithms for CTL, and fair CTL. The mu-calculus is discussed and its complexity is analysed. 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.
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 and the
modal mu-calculus
- 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.
Assessment
The assessment consists of two assignments and a written examination. The weighting of the assignments and the examination are 30% and 70%, respectively. Students can successfully pass the course if a minimal score of 5.5 for the written examination is obtained and the average of both assignments is at least 5.5.
Important Notes
- Lectures are Monday afternoon (quartile A) 15.45 -- 17.30 in Aud 14, TU/e, and Friday afternoon (quartile A) 13.45 -- 15.30 in Aud 15.
- Note: first lecture is Friday 7 September. There are no lectures on Friday 21 September, Monday 8 October and Friday 19 October. Last lecture is Friday 26 October.
- The exam is on 30 October, 9.00-12.00. There is a retry on 21 January 2013, 9.00-12.00.
- 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.
- The 2012 lectures of this course will be recorded and can be viewed online
Course material
- Additional reading (not mandatory, roughly covers the first 4 lectures): Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. MIT Press, ISBN 0-262-03270-8.
- More additional reading (not mandatory either, roughly covers the first 3 lectures): Principles of Model Checking. Christel Baier and Joost-Pieter Katoen. MIT Press, ISBN 978-0-262-02649-9.
- Handouts, which are available for download below (updated regularly):
- 7 Sep: domestic announcements can be downloaded here.
- 17 Sep: E. Allen Emerson: Model Checking and the Mu-calculus, 1996.
- 24 Sep: A. Mader: Verification of Modal Properties Using Boolean Equation Systems, 1997.
- 28 Sep: J.J.A. Keiren: An experimental study of algorithms and optimisations for parity games, with an application to Boolean Equation Systems, 2009.
- 01 Oct: O. Friedmann, Recursive solving of parity games requires exponential time, 2011
- 05 Oct: M. Jurdzinski, Small Progress Measures for Solving Parity Games, 2000
- 05 Oct: S. Schewe, Solving Parity Games in Big Steps, 2007
- 12 Oct: J.F. Groote, T.A.C. Willemse, Model-checking processes with data, 2005 (note: there is a subtle mistake in the Par function in that paper; take the definition from the slides)
- 22 Oct: B. Ploeger, J.W. Wesselink, T.A.C. Willemse, Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems, 2011.
- 22 Oct: S. Orzan, T.A.C. Willemse, Static Analysis Techniques for Parameterised Boolean Equation Systems, 2009.
- Assignments were made available for download below.
Topics and Course notes
Part I: (exercises can be downloaded from here)
- 07 Sep: The temporal logics CTL*, CTL and LTL: syntax and semantics (slides)
- 10 Sep: Symbolic Model Checking for CTL (slides)
- 14 Sep: Symbolic Model Checking: Fairness and Counterexamples (slides)
- 17 Sep: The mu-calculus (slides)
- 24 Sep: Boolean Equation Systems (slides)
- 28 Sep: Parity Games (slides)
- 01 Oct: Solving Parity Games Recursively (slides), lecturer: Jeroen Keiren
- 05 Oct: Solving Parity Games using Small Progress Measures and Bigstep (slides), lecturer: Jeroen Keiren
