**2IMF35 --- Algorithms for Model Checking (2016-2017)**

*"Given a model of a system, exhaustively and automatically check whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.*" (source: Wikipedia).

Model checking has applications in a diversity of areas such as software and hardware verification (as expected), but also in

*planning*,

*scheduling*,

*mechanical engineering, business process mining*and

*biology*. To understand the limitations of model checking, we study the mu-calculus, CTL* and some of its subsets such as LTL and CTL, from a computational viewpoint in these lectures. 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 able to reason
about Parity Games
- 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 iff a minimal score of

**5.5**for the written examination is obtained and the

**average**of both assignments is at least

**5.5**. In that case, the grade is determined by the weighting of the assignments and the examination. In case the minimal score is less than

**5.5**for either the examination or the assignment, the minimal score of these determines the final grade.

**Important Notes**

- Lectures are Monday afternoon (quarter 3) 15.45
-- 17.30 in
**Auditorium 10**, and Wednesday morning (quarter 3) 10.45 -- 12.30 in Auditorium 16; quite comfortable hours... -
Note: first lecture is
**Monday 6 February**. There are no lectures on 27 February and**1 March**. Last lecture is**Wednesday 22 March**. **Office hours**for discussing the course: on Wednesday from 13.30-14.00. Be sure to drop me a mail if you wish to ensure I'm in my office.- The exam is on Monday 10 April,
13.30-16.30. There is a resit on Friday 7 July, 18.00-21.00 (but I
strongly suggest you pass the first
exam).
- 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 have been recorded and can be viewed online (you do need to log in for this and be with an institute that struck the right kind of deal with the TU/e for this; the recordings seems to leave some room for improvement).
- Look for previous
incarnations of this course (then assigned the number 2IW55) for some
**exams with solutions**(see teaching/past courses; the exams from 2010 can be found online, as well as a 2009 version)

**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, but offers a very nice read otherwise): Principles of Model
Checking. Christel Baier and Joost-Pieter Katoen. MIT Press, ISBN
978-0-262-02649-9.
- Handouts,
which will be made available for download below (updated
regularly).
- 15 Feb: E.A. Emerson and C.-L. Lei: Model Checking in the Propositional Mu-Calculus
- 20 Feb: A. Mader: Verification of Modal Properties Using Boolean Equation Systems
- 22 Feb: J.J.A. Keiren: An experimental study of algorithms and optimisations for parity games, with an application to Boolean Equation Systems
- 06 Mar: M. Gazda and T.A.C. Willemse: Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds
- 06 Mar: O. Friedmann: Recursive solving of parity games requires exponential time
- 08 Mar: M. Jurdzinski: Small Progress Measures for Solving Parity Games
- 08 Mar: M. Gazda, T.A.C. Willemse: Improvement in Small Progress Measures
- 13 Mar: B. Ploeger, J.W. Wesselink, T.A.C. Willemse: Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems
- 13 Mar: J.F. Groote, T.A.C. Willemse: Parameterised Boolean Equation Systems
- 15 Mar: S. Cranen, B. Luttik and T.A.C. Willemse: Proof Graphs for Parameterised Boolean Equation Systems
- 15 Mar: J.F.
Groote and T.A.C. Willemse: Model-checking processes with
data (note: there is a subtle mistake in the Par function in
that paper; take the definition from the
slides)

- Assignments.
Yes, these too, two of'em, will be made available for download below.
Assignments will be briefly introduced/explained during the lectures.
**Caution: the assignments involve some programming and take time. Plan carefully. Assignments can be made in small groups (3 students max).** - Assignment I can no longer be downloaded. Deadline for handing in report is Friday 10 March.
- Assignment II
can no longer be downloaded.
Deadline for handing in report is Friday 31
March.
**Research.**If (you think) you enjoy doing research (individually or in a small group) in the intersection of algorithms, logics, game theory or their application, feel free to contact me (or approach me during the lectures): I might have some topics that interest you. Of course, you can also propose your own topics.

**Topics and Course notes**

*Part I: 06 Feb - 15 Feb. Exercises (to exercise your skills; not mandatory) can be downloaded from here*

- 06 Feb: Domestic Announcements (slides) and the temporal logics CTL*, CTL and LTL (slides)
- 08 Feb: Symbolic model checking for CTL (slides)
- 13 Feb: Symbolic model checking: Fairness and Counterexamples (slides)
- 15 Feb: The mu-calculus (slides)

*Part II: 20 Feb - 8 Mar: Boolean Equation Systems and Parity Games*

- 20 Feb: Boolean equation systems (slides)
- 22 Feb: Parity Games (slides)
- 06 Mar: Solving parity games recursively (slides)
- 08 Mar: Small Progress Measures for Solving Parity Games (slides)

*Part III: 13 Mar - 22 Mar: Parameterised Boolean Equation Systems*

- 13 Mar: Parameterised
Boolean equation systems (I) (slides)
- 15 Mar: Parameterised Boolean equation systems (II) (slides)
- 20 Mar: Parameterised Boolean equation systems (III) (slides)
- 22 Mar: Closing (slides)

*Exercise
class: 29 March (exercises can be downloaded here); there are no
lectures on 27 March.*

*Worked out
exam from 2014-2015 can be downloaded here; use at your own
risk, there may be typos or worse in the
solutions!*

*In case you missed it,
the exam from 10 April can be downloaded here, and its solution
here (again at your
own risk, these will contain typos and may contain
worse)*