Modeling and Verification of Probabilistic Systems


  • 18.8.2014: Please find schedules for the days of the exams below. The scheduled times are sine tempore. Please consider arriving a few minutes in advance.
  • 15.7.2014: It is our pleasure to inform you that everyone is admitted to the exam.
  • 14.7.2014: Please find a summarized version of the evaluation results for both the lecture and the exercises below.
  • 14.7.2014: Please find information on the dates of the exams below.
  • 27.5.2014: As Prof. Katoen has an important appointment,  today’s lecture has to be cancelled.


Type Day Time Room Start Lecturer
Lecture Tue 13:00 – 14:30h 9U10, E3 April 15 Katoen
Thu 13:00 – 14:30h 9U10, E3 April 17 Katoen
Exercise Thu 15:00 – 16:30h 9U10, E3 April 24 Jansen / Kaminski


The aim of this course is to address the compositional modeling and the automated verification (i.e., model checking) of probabilistic models. These models are important for addressing performance aspects, they are the key to randomised distributed algorithms, and have applications in systems biology as well as security, to mention a few. This course is about:

  1. How to obtain models for complex systems that involve random aspects?
  2. How to verify in a fully algorithmical manner, whether such models satisfy basic properties, such as reachability probabilities?
  3. Can we make these models smaller to enable or simplify verification?
  4. What kind of practical problems can be treated in this manner?

If you’d like to have an introductory read on this lecture, then you might consider to read the recent paper called “Model Checking Meets Probability: A Gentle Introduction” by Joost-Pieter Katoen. Moreover, the paper “Performance Evaluation and Model Checking Join Forces”  published in Communications of the ACM (2010) might be of interest.


Markov chains, Markov decision processes, probabilistic automata, interactive Markov chains, model checking, probabilistic temporal logic (CTL and LTL), bisimulation, compositional modeling, concurrency, compositional minimisation.


No. Date Subject Slides
1 April 15 Probability Theory Refresher Lecture 1
2 April 17 Discrete-Time Markov Chains Lecture 2
3 April 22 Reachability Probabilities Lecture 3
4 April 24 Qualitative Properties Lecture 4
5 April 29 Omega-regular Properties Lecture 5
6 May 8 PCTL Model Checking Lecture 6
7 May 13 Qualitative PCTL Lecture 7
8 May 15 Probabilistic Bisimulation Lecture 8
9 May 20 Markov Decision Processes Lecture 9
10 May 22 Reachability Probabilities in MDPs Lecture 10
11 May 27 Reachability Probabilities in MDPs (cont’d)
12 June 5 Verifying MDPs against PCTL Lecture 12
13 June 17 Continuous-Time Markov Chains Lecture 13
14 June 24 Transient Analysis of CTMCs Lecture 14
15 June 26 Timed Reachability in CTMCs Lecture 15
16 July 1 CSL Model Checking Lecture 16
17 July 3 Probabilistic Automata
18 July 8 Probabilistic Automata (cont’d)
19 July 10 Markov Automata Lecture 19
20 July 15 Markov Automata (cont’d) Lecture 20


No. Due Exercise Solution
1 April 24 Series 1 Solution 01
2 April 30 Series 2 Solution 02
3 May 15 Series 3 Solution 03
4 May 22

Series 4

Solution 04
5 June 5 Series 5 Solution 05
6 June 17 Series 6 Solution 06
7 June 26 Series 7 Solution 07
8 July 3 Series 8 Solution 08
9 July 10 Series 9 Solution 09


The exam will be in the form of an oral exam. For the oral exam, you will be given one hour of silent work to prepare solutions for two tasks. Afterwards you are to present your solutions and you will be asked a few additional questions.

There is a choice of two possible dates to take this exam on: August 25 (first slot at 10:30h) and September 26 (first slot at 8:30h). Please let Benjamin know on which date you would like to take the exam until August 18 (or way earlier). Additionally, you may provide information on whether you want to be scheduled for one of the earlier or one of the later slots of your preferred exam day. Such additional information will of course be considered on a first-come-first-serve basis.

Exam Schedules

Please arrive at the scheduled time at our seminar room (room 4201b).

August 25

Time Student
9:30 Quatmann
10:00 Florian
11:30 Mroz
12:00 Wohnout
12:45 Weiand
13:15 Korzeniewski
14:00 Prinz

September 26

Time Student
8:30 Berger

Evaluation results

Further information

  • The course will be entirely given in English.
  • There are no lecture notes (yet); the course material will consist of slides.
  • The exam will be awarded with 6 ECTS credits. Details will follow later.

Additional background literature

  • C. Baier and J.-P. Katoen. Principles of Model Checking, MIT Press, 2008 [Chapter 10].
  • H.C. Tijms: A First Course in Stochastic Models. Wiley, 2003.
  • H. Hermanns: Interactive Markov Chains: The Quest for Quantified Quality. LNCS 2428, Springer 2002.
  • E. Brinksma, H. Hermanns, J.-P. Katoen: Lectures on Formal Methods and Performance Analysis. LNCS 2090, Springer 2001.