News
- 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.
Schedule
| 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 |
Overview
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:
- How to obtain models for complex systems that involve random aspects?
- How to verify in a fully algorithmical manner, whether such models satisfy basic properties, such as reachability probabilities?
- Can we make these models smaller to enable or simplify verification?
- 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.
Topics
Markov chains, Markov decision processes, probabilistic automata, interactive Markov chains, model checking, probabilistic temporal logic (CTL and LTL), bisimulation, compositional modeling, concurrency, compositional minimisation.
Slides
| 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 |
Exercises
| 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 | 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 |
Exam
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.