News
- 19.2.2019: The exam inspection will take place at Thursday 28 February from 13.00 to 14.00​ in our seminar room (Room 4201b​​​).
- 14.1.2019: We fixed two issues with exercise 4 of the current sheet. Please make sure that you have the correct version of the sheet (all actions should be internal and the probabilities for all actions should sum up to one).
- 8.1.2019: There is no exercise class on 9 January (tomorrow).
- 18.12.2018: The problems with RWTH Online seem to be resolved, so please register for the exam as soon as possible. In case of any problems, let us know.
- 11.09.2018:We are online.
Schedule
| Type | Day | Time | Room | Start | Lecturer |
|---|---|---|---|---|---|
| Lecture | Mon | 10:30 – 12:00h | 5056 | 8. 10. | Katoen |
| Tue | 08:30 – 10:00h | 5056 | 9.10. | Katoen | |
| Exercise | Wed | 14:30 – 16:00h | AH VI | 24.10. | Spel, Quatmann |
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 algorithmic manner, whether such models satisfy basic properties, such as reachability probabilities?
- Can we make these models smaller to enable or simplify their 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 paper “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, Markov automata (aka: continuous-time MDPs), model checking, probabilistic temporal logic (probabilistic CTL and LTL), bisimulation, compositional modeling, concurrency, compositional minimisation.
Slides
| No. | Date | Subject | Slides | Notes |
|---|---|---|---|---|
| 1 | 8.10 | Introduction/Probability Refresher | mvps2018_lec01 | |
| 2 | 9.10 | Discrete-Time Markov Chains | mvps2018_lec02 | notes02 |
| 3 | 15.10 | Reachability Probabilities | mvps2018_lec03 | notes03 |
| 4 | 22.10 | Qualitative Properties | mvps2018_lec04 | notes04 |
| 5 | 23.10 | Verifying Linear-Time Properties (1) | mvps2018_lec05 | notes05-6 |
| 6 | 29.10 | Verifying Linear-Time Properties (2) | ||
| 7 | 30.10 | Probabilistic CTL | mvps2018_lec07 | notes07 |
| 8 | 5.11 | Qualitative PCTL versus CTL | mvps2018_lec08 | notes08 |
| 9 | 6.11 | Probabilistic Bisimulation (1) | mvps2018_lec09 | notes09+10 |
| 10 | 12.11 | Probabilistic Bisimulation (2) | ||
| 11 | 13.11 | Markov Decision Processes | mvps2018_lec11 | notes11 |
| 12 | 19.11 | Reachability Probabilities in MDPs (1) | mvps2018_lec12 | notes12 |
| 13 | 20.11 | Reachability Probabilities in MDPs (2) | ||
| 14 | 26.11 | MDP Model Checking | mvps2018_lec14 | notes14 |
| 15 | 27.11 | Continuous-Time Markov Chains | mvps2018_lec15 | notes15 |
| 16 | 4.12 | Transient Analysis in CTMCs | mvps2018_lec16 | notes16 |
| 17 | 10.12 | Timed Reachability in CTMCs | mvps2018_lec17 | notes17+18 |
| 18 | 11.12 | |||
| 19 | 17.12 | Probabilistic Automata | notes19+20 | |
| 20 | 18.12 | Compositional Minimisation | ||
| 21 | 07.01 | Markov Automata | mvps2018_lec21+22 | |
| 22 | 08.01 | |||
| 23 | 14.01 | Multi-Objective Verification on MDPs | mvps2018_lec23 | |
| 24 | 15.01 | Parameter Synthesis | mvps2018_lec24 |
Exercises
| No. | Due | Exercise |
|---|---|---|
| 1 | 24.10. | ex01 |
| 2 | 31.10. | ex02 |
| 3 | 07.11. | ex03 |
| 4 | 14.11. | ex04 |
| 5 | 21.11. | ex05 |
| 6 | 28.11. | ex06 |
| 7 | 05.12. | ex07 |
| 8 | 12.12. | ex08 |
| 9 | 19.12. | ex09 |
| 10 | 16.01. | ex10 |
| 11 | 30.01 | ex11 |
Further information
- The course will be entirely given in English.
- There are no lecture notes (yet); the course material will consist of slides.
- The written exam will be awarded with 6 ECTS credits.
- The exam dates are: February 18, 2019 (10:00-12:00) and March 13, 2019 (10:00-12:00)
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.
- J.-P. Katoen. The Probabilistic Model Checking Landscape. LICS 2016.
- 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.
- M. Stoelinga: Introduction to Probabilistic Automata. Bulletin of the EATCS 78. 2002
- M. Timmer: Efficient Modelling, Generation and Analysis of Markov Automata. Chapter 3. 2013