Introduction to Model Checking


  • Friday 17.01.2020 will be the last lecture. Last exercise class is on Friday, 31.01.2020.
  • 16.12.19: Due to inconsistencies, we updated the lecture slides 12+13 and 15 in Moodle
  • 12.12.19: No Lectures on 13.12.19 and 20.12.19!
  • In accordance with what we announced during the exercises, we changed the rules of what you can bring to the exam.
    You may bring one A4, two sided, handwritten, containing anything you want.
    Why? We are not in a position to provide enough books, and to save the environment (a bit) we decided that it is not wise to have everyone print the lecture slides. 
  • 22.11.19: Due to the “Tag der Informatik”, on December, 6th there won’t be any lecture or exercise!
  • 25.10.19: No lecture on Thursday (31.10) as already announced in the lecture.
  • 25.10.19: No lecture and exercise class on Friday (1.11) as this is holiday.
  • 16.10.19: The lecture on Friday (18.10) will be cancelled.
  • 16.10.19: First exercise sheet online.
  • 10.10.19: Lecture slides with annotations only available in Moodle!
  • 26.09.19: We are online.


Type Day Time Hall Start Lecturer
Lecture Thu 10:30 – 12:00 AH II 10.10 Katoen
  Fri 14:30 – 16:00 AH III 11.10 Katoen
Exercise Fri 10:30 – 12:00 5056 25.10 Junges / Klinkenberg


No. Date Topic Slides
1 10.10.2019 Introduction/ Motivation l01.pdf
2 11.10.2019 Transition Systems l02.pdf
3 17.10.2019 LT-Properties l03.pdf
4 24.10.2019 Omega-regular Properties  l04.pdf
5 25.10.2019 B├╝chi Automata l05.pdf
6 07.11.2019 Verifying Omega-regular Properties l06.pdf
7 08.11.2019 Linear Time Logic l07.pdf
8 14.11.2019 LTL Model Checking l08.pdf
9 15.11.2019 Complexity of LTL Model Checking l09.pdf
10 21.11.2019 Computation Tree Logic l10.pdf
11 22.11.2019 CTL Model Checking l11.pdf
12 28.11.2019 Branching Time vs Linear Time l12.pdf
13 29.11.2019 – ” – – ” –
14 05.12.2019 Fairness in Model Checking l13.pdf
15 12.12.2019 Bisimulation Quotienting l14.pdf
16 09.01.2019 Partial Order Reduction l15.pdf
17 10.01.2019 Reduced Ordered Binary Decision Diagrams l16.pdf
18 16.01.2019 Symbolic Model Checking With BDDs l17.pdf
19 17.01.2019 Symbolic Model Checking with SAT l18.pdf


No. Handed Out On Date Due Exercise Sheet
 1 16.10.2019 25.10.2019 ex01.pdf
2 25.10.2019 08.11.2019 ex02.pdf
3 10.11.2019 15.11.2019 ex03.pdf
4 15.11.2019 22.11.2019 ex04.pdf
5 22.11.2019 29.11.2019 ex05.pdf
6 05.12.2019 13.12.2019 ex06.pdf
7 13.12.2019 20.12.2019 ex07.pdf
8 04.01.2020 10.01.2020 ex08.pdf
9 10.01.2020 17.01.2020 ex09.pdf
10 24.01.2020 31.01.2020 ex10.pdf


  Date Time Location
First exam 20.02.2020 14:30-16:30 Aula 2 (2352|021)
Re-exam 13.03.2020 14:30-16:30 Aula 2 (2352|021)

You are allowed to bring one a4, two sided, handwritten containing your own notes.


In 2008, the ACM awarded the prestigious Turing Award – the Nobel Prize in Computer Science – to the pioneers of Model CheckingEd ClarkeAllen Emerson, and Joseph Sifakis.
a83b7b5493 e43fc9f119 c0dc5e8b7f

Because model checking has evolved in the last twenty-five years into a widely used verification and debugging technique for both software and hardware.

It is used (and further developed) by companies and institutes such as IBM, Intel, NASA, Cadence, Microsoft, and Siemens, to mention a few, and has culminated in a series of mostly freely downloadable software tools that allow the automated verification of, for instance, C#-programs or combinational hardware circuits.

Subtle errors, for instance due to multi-threading, that remain undiscovered using simulation or peer reviewing can potentially be revealed using model checking.  Model checking is thus an effective technique to expose potential design errors and improve software and hardware reliability.

But how does it work, that is, what are its underlying principles?
That’s exactly the focus of this lecture series!

We will show that model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures.  Its complexity is analyzed using standard techniques from complexity theory.

Contents of the Lecturemodelchecking

Model checking is based on, well, checking models. So, we first start by explaining what models are, and will make clear that so-called labeled transition systems, a model that is akin to automata, are suitable for modeling sequential, as well as multi-threading programs.

This is followed by a detailed study on various classes of system properties such as safetyliveness, and fairness.  It will be shown how finite automata as well as variants thereof that accept infinite words are suitable for verifying regular properties.

The linear-time and branching time temporal logics LTL and CTL are then introduced and compared. Model checking algorithms for these logics together with detailed complexity considerations are covered.

Finally, abstraction techniques based on bisimulation and simulation relations are covered. These techniques are at key techniques to combat the state explosion problem.


This course is suitable for  bachelor (this course is part of the “Wahlkatalog” in theoretical computer science) and master students.

We expect students to have some basic knowledge in:

  • Automata Theory
  • Mathematical Logic
  • Discrete Mathematics
  • Complexity Theory
  • Algorithms and Data Structures

The course book (see below) will contain a summary of the issues in these areas that are relevant to this lecture series.  We believe that this course is also well-suited for students in electrical engineeering and mathematics.


The lectures and all materials are in english. The slides will be made available via this webpage during the course.

The course is based on:

Principles of Model Checking
by Christel Baier and Joost-Pieter Katoen
MIT Press, 2008.

An errata document to the book may be found here.

It is possible to buy a book (about 40 euros), but there is no need to do so as there are various copies of the book available at the CS library.

The course will basically cover Chapters 1 through 7 (upto section 7.3).

Additional literature:

  • E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999
  • M. Huth and M.D. Ryan: Logic in Computer Science – Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004
  • K. Schneider: Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004