Introduction to Model Checking


  • There will be no lectures on June 19 and June 26 (Sommerfest).
  • There will be no lecture on 4th May. The next lecture will be on the 8th of May.
  • 2015-03-01: we are online!


Type Day Time Hall Start Lecturer
Lecture Mon 12:15 – 13:45 AH I Apr 13 Katoen
Fri 14:00 – 15:30 AH III Apr 10 Katoen
Exercise Wed 13:30 – 15:00 9U10 Apr 22 Chakraborty / Jansen


No. Date Subject/Slides Exercises Solutions
1 10th Apr
2 13th Apr Modelling parallel systems (1) Ex 01 Sol 01
3 17th Apr Modelling parallel systems (2)
4 20th Apr Channel systems Ex 02 Sol 02
5 24th Apr Linear time properties
6 27th Apr Invariants and safety Ex 03 Sol 03
7 8th May Liveness and fairness
8 11th May Regular properties Ex 04 Sol 04
9 15th May Omega-regular properties
10 18th May Verifying omega-regular properties Ex 05 Sol 05
11 22nd May Linear temporal logic (1)
12 1st June Linear temporal logic (2) Ex 06 Sol 06
13 5th June LTL model checking
14 8th June

Complexity of LTL model checking(1)

Complexity of LTL model checking(2)

Ex 07 Sol 07
15 12th June Computation Tree Logic
16 15th June Expressiveness of CTL and LTL Ex 08 Sol 08
17 22nd June CTL model checking
18 29th June

CTL with fairness(1)

CTL with fairness(2)

19 3rd July Extensions to CTL
20 6th July Bisimulation equivalence Ex 09 Sol 09
21 10th July Bisimulation and CTL* Equivalence


In 2008, the ACM awarded the prestigious Turing Award – the Nobel Prize in Computer Science – to the pioneers of Model Checking: Ed Clarke, Allen 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 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 safety, liveness, 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