**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.

**Objectives**

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)

*Part II: (exercises for Part II and III can be downloaded from here)*

- 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

*Part III:*