FOR UPTODATE INFORMATION REGARDING THE PROGRAMME, SEE THE END OF THIS PAGE
2IMF35  Algorithms for Model Checking
"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 finitestate 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 mucalculus, 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 mucalculus is discussed and its complexity is analysed. Transformations of the mucalculus 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
Assessment
The assessment consists oftwo three assignments and a written examination. The weighting of the first two practical
assignments and the individual third assignment examination are 30% and 70%, respectively. Students
can successfully pass the course iff a minimal score of 5.5 for the third assignment
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 third assignment examination. In case the minimal score is less than 5.5 for either the individual assignment examination or the practical assignment, the minimal score of these determines the final grade.
Important Notes
Course material
Topics and Course notes
Part I: 03 Feb  12 Feb. Exercises (to exercise your skills; not mandatory) can be downloaded from here
2IMF35  Algorithms for Model Checking
"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 finitestate 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 mucalculus, 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 mucalculus is discussed and its complexity is analysed. Transformations of the mucalculus 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 mucalculus
 be capable of transforming (fair) CTL formulae to the modal mucalculus
 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 mucalculus
 be able to transform the problem of model checking to the modal mucalculus 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
Important Notes
 Lectures are Monday afternoon (quarter 3) 15.30  17.15 in Atlas 2.215, and Wednesday morning (quarter 3) 10.45  12.30 in Atlas 6.208; quite comfortable hours and seemingly decent locations...
 Note: first lecture is Monday 3 February. There are no lectures on 24 February and 26 February. Last lecture is (tentatively) Wednesday 18 March.
 Office hours for
discussing the course: on Wednesday from 13.3014.00. Be sure to drop me a mail if you wish to ensure I'm in my
office. I live in MF 6.073.
 The exam is on Saturday(?!) 18 April, 13.3016.30. There is a resit on Friday 3 July, 18.0021.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 seem 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; e.g. the exams from 2016 and 2010 can be found online, as well as a 2009 version)
 Last year's student questionnaire can be downloaded here
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 0262032708. The second edition of the same book, by an extended set of authors, significantly improves on the first edition and I would advise getting a hold on that one if you're purchasing books.
 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 JoostPieter Katoen. MIT Press, ISBN
9780262026499.
 Handouts, which will be made available for download below (updated regularly).
 12 Feb: E.A. Emerson and C.L. Lei: Model Checking in the Propositional MuCalculus
 17 Feb: A. Mader: Verification of Modal Properties Using Boolean Equation Systems
 19 Feb: J.J.A. Keiren: An experimental study of algorithms and optimisations for parity games, with an application to Boolean Equation Systems
 02 Mar: O. Friedmann: Recursive solving of parity games requires exponential time
 04 Mar: M. Jurdzinski: Small Progress Measures for Solving Parity Games
 04 Mar: M. Gazda, T.A.C. Willemse: Improvement in Small Progress Measures
 09 Mar: B. Ploeger, J.W. Wesselink, T.A.C. Willemse: Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems
 09 Mar: J.F. Groote, T.A.C. Willemse: Parameterised Boolean Equation Systems
 11 Mar: S. Cranen, B. Luttik and T.A.C. Willemse: Proof Graphs for Parameterised Boolean Equation Systems
 23 Mar: S. Orzan and T.A.C. Willemse: Static Analysis Techniques for Parameterised Boolean Equation Systems
 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 and preferred).
 Assignment I can be downloaded here. Deadline for handing in the report is Friday 13 March (scroll down for the alternative assignment in case this applies to you).
 Assignment II can be downloaded here. Deadline for handing in the report is Friday 3 April (scroll down for the alternative assignment in case this applies to you).
 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: 03 Feb  12 Feb. Exercises (to exercise your skills; not mandatory) can be downloaded from here
 03
Feb: Domestic Announcements (slides) and the
temporal logics CTL*, CTL and LTL (slides)
 07 Feb: Symbolic model checking for CTL (slides)
 10 Feb: Symbolic model checking: Fairness and Counterexamples (slides)
 12 Feb: The modal mucalculus (slides)
 group assignment I (slides of the announcement and the actual assignment description itself); contact me if you are still a singleton group...
 original EmersonLei paper; some notes by Jeroen Keiren on the mucalculus
 alternative assignment for those that did last year's assignment
 17 Feb: Boolean Equation Systems (slides)
 19 Feb: Parity Games (slides)
 02 Mar: Solving parity games recursively (slides)
 04 Mar: Small Progress Measures for Solving Parity Games (slides)
 group assignment II (slides of the announcement and the actual assignment description itself); contact me if you are still a singleton group...
 original Jurdzinski paper
 alternative assignment for those that did last year's assignment
 09 Mar: Parameterised Boolean Equation Systems I (slides)
 11 Mar: Parameterised Boolean Equation Systems II (slides)
 23 Mar: Parameterised Boolean Equation Systems III: (slides).
Please watch the 2012 video lectures of 2IW55, lectures 11 and 12; see here  25 Mar: Q&A organised via Canvas Conferences (we stick to regular hours: 10.4512.30)
Files for download: slides and exercises (and their solutions)  30 Mar: Q&A organised via Canvas Conferences
Please come prepared: try to answer the questions contained in the following document: exercises
Note: Due to the Coronavirus precautions taken by the University, the threehour written exam will be replaced by an individual takehome assignment. Deadline for handing in: 18 April, 12.00. The assignment can accessed via the Canvas course page (and should also be handed in via the same).