2IW55 --- 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 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.
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 morning (quartile A) 8.45 -- 10.30 (I know... quite a challenge) in Aud 14, TU/e, and Thursday afternoon (quartile A) 15.45 -- 17.30 in Aud 14 (quite the challenge, too).
- Note: first lecture is Monday 2 September. There are no lectures on Monday 16 September and Thursday 19 September, and on Monday 7 October and Thursday 10 October. Last lecture is Thursday 24 October.
- Office hours
for discussing the course: on Monday from 11.15-12.00 and on Friday from
9.15-10.00. Drop me a mail if you wish to ensure I'm in my
office.
- The exam is on Wednesday 30
October, 9.00-12.00. There is a retry on Tuesday 21 January 2014,
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 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).
- Look for previous
incarnations of this course 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).
- 12 Sep: E.A. Emerson: Model Checking and the Mu-calculus, 1996.
- 23 Sep: A. Mader: Verification of Modal Properties Using Boolean Equation Systems, 1997.
- 26 Sep: J.J.A. Keiren: An experimental study of algorithms and optimisations for parity games, with an application to Boolean Equation Systems, 2009.
- 30 Sep: M. Gazda and T.A.C. Willemse: Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds, 2013.
- 30 Sep: R. Küster: Memoryless Determinacy of Parity Games, 2002.
- 03 Oct: H. Klauck: Algorithms for Parity Games, 2002.
- 14/17 Oct: J.F. Groote and 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).
- 17 Oct: S. Cranen, B. Luttik and T.A.C.
Willemse, Proof Graphs
for Parameterised Boolean Equation Systems,
2013.
- 17/21 Oct: B. Ploeger, J.W. Wesselink, T.A.C. Willemse, Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems, 2011.
- 21 Oct: S. Orzan,
T.A.C. Willemse, Static
Analysis Techniques for Parameterised Boolean Equation
Systems,
2009.
- Assignments.
Yes, these too, two of'em, were made available for download below.
- 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 have some topics that might interest you. Of course, you
can also propose your own
topics.
Topics and Course notes
Part I: 02 Sep - 12 Sep. Exercises can be downloaded from here
- 02 Sep: Domestic Announcements (slides) and the temporal logics CTL*, CTL and LTL (slides)
- 05 Sep: Symbolic model checking for CTL (slides; note: these now contain proof sketches of two statements so you can check these at your leisure)
- 09 Sep: Symbolic model checking: Fairness and Counterexamples (slides)
- 12 Sep: The mu-calculus (slides)
- 23
Sep: Boolean Equation Systems (slides,
updated)
- 26 Sep: Parity Games (slides)
- 30 Sep: Recursively Solving Parity Games (slides); guest lecturer: Maciej Gazda
- 03 Oct: Small Progress Measures (slides); guest lecturer: Maciej Gazda
Part III: 14 Oct - 24 Oct.
- 14 Oct: Parameterised
Boolean Equation Systems 1 (slides,
updated)
- 17 Oct: Parameterised Boolean
Equation Systems 2 (slides, updated with
examples)
- 21 Oct: Parameterised Boolean
Equation Systems 3 (slides)
- 24
Oct: Wrap-up (slides)