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

- 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 (not mandatory, 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 (not mandatory either, roughly covers the first 6 lectures): Principles of Model Checking. Christel Baier and Joost-Pieter Katoen. MIT Press, ISBN 978-0-262-02649-9.
- Handouts.

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 A. Mader
- week 9-10:
- Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems by B. Ploeger, J.W. Wesselink and T.A.C. Willemse
- Static Analysis Techniques for Parameterised Boolean Equation Systems by S. Orzan, J.W. Wesselink and T.A.C. Willemse
- Parameterised Boolean Equation Systems by J.F. Groote and T.A.C. Willemse
- week 11-13:

Topics and course notes

Part I: (Exercises can be downloaded here)

- 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: Fair Symbolic Model Checking and Counterexamples (slides)
- week 5: Equivalences and Pre-orders: State Space Reduction and Preservation of Properties (slides)
- week 6: CTL* Exercises

Part II: (Additional exercises can be downloaded here)

- week 7: The mu-Calculus (slides)
- week
8: Boolean Equation Systems (slides).
Example BES files for experimenting, the grammar and their (partial)
solutions are contained in this
archive.
- week 9: Parameterised Boolean Equation Systems (slides)
- week 10: Parameterised Boolean Equation Systems (slides)
- week 11: Parity Games (slides), guest lecturer: Jeroen Keiren
- week 12: Recursive Algorithm for Parity Games (slides), guest lecturer: Jeroen Keiren
- week 13: Small Progress Measures for Parity Games (slides), guest lecturer: Jeroen Keiren
- week 14: mu-calculus
exercises

For the '07--'10 pages, see here, here, here and here. For the early years (< '07), see here.