News
- 13.11.2015: We fixed a mistake in the exercise. When listing probabilities for the given properties, one should use a maximizing scheduler.
- 26.11.2015: Due to technical problems, we uploaded the files slightly later. [now fixed]
- 26.10.2015: Please note that task 1c) of sheet 1 has slightly changed.
- 21.10.2015: The exercise class will be taking place on Wednesdays in the seminar room of i2, that is room 4201b in E1.
- 19.10.2015: [Important] Due to collisions with other courses, the time and place of Tuesday’s lectures has permanently shifted to 14.15 at 9U10 (in the basement of building E3).
- 08.09.2015: We are online.
Schedule
| Type | Day | Time | Room | Start | Lecturer |
|---|---|---|---|---|---|
| Lecture | Tue | 14:15 – 15:45h | 9U10 (E3) | Oct 27 | Katoen |
| Wed | 10:15 – 11:45h | 5052 | Oct 21 | Katoen | |
| Exercise | Wed | 14:15 – 15:45h | Seminar Room i2 (4201b) | Oct 28 | Dehnert / Junges |
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 | Oct 21 | Probability Theory Refresher | slides_mvps2015_lecture1.pdf |
| 2 | Oct 27 | Markov Chains | slides_mvps2015_lecture2.pdf |
| 3 | Oct 28 | Reachability Probabilities | slides_mvps2015_lecture3.pdf |
| 4 | Nov 3 | Almost-Sure Properties | slides_mvps2015_lecture4.pdf |
| 5 | Nov 4 | Verifying Probabilistic LTL | slides_mvps2015_lecture5.pdf |
| 6 | Nov 10 | PCTL Model Checking | slides_mvps2015_lecture6.pdf |
| 7 | Nov 11 | Qualitative PCTL | slides_mvps2015_lecture7.pdf |
| 8+9 | Nov 17+18 | Probabilistic Bisimulation | slides_mvps2015_lecture8.pdf |
| 10 | Nov 24 | Markov Decision Processes | slides_mvps2015_lecture10.pdf |
| 11 | Nov 25 | Reachability Probabilities in MDPs | slides_mvps2015_lecture11.pdf |
| 12 | Dec 2 | PCTL Model Checking on MDPs | slides_mvps2015_lecture12.pdf |
| 13 | Dec 8 | Continuous-Time Markov Chains | slides_mvps2015_lecture13.pdf |
| 14 | Dec 9 | Transient Analysis in CTMCs | slides_mvps2015_lecture14.pdf |
| 15 | Dec 15 | Timed Reachability Probabilities | slides_mvps2015_lecture15.pdf |
| 16 | Dec 16 | Timed PCTL Model Checking | slides_mvps2015_lecture16.pdf |
| 17 | Jan 13 | Probabilistic Automata | |
| 18 | Jan 19 | Probabilistic Automata (continued) | |
| 19 | Jan 26 | Markov Automata | |
| 20 | Jan 27 | Markov Automata (continued) | |
| 21 | Feb 9 | Applications |
Exercises
| No. | Due | Exercise | Solution |
|---|---|---|---|
| 1 | Oct 28 | ex01 | sol01 |
| 2 | Nov 4 | ex02 | sol02 |
| 3 | Nov 11 | ex03 | sol03 |
| 4 | Nov 18 | ex04 | sol04 |
| 5 | Nov 25 | ex05 | sol05 |
| 6 | Dec 02 | ex06 | sol06 |
| 7 | Dec 09 | ex07 | sol07 |
| 8 | Dec 16 | ex08 | sol08 |
| 9 | Jan 13 | ex09 | sol09 |
| 10 | Jan 27 | ex10 | sol10 |
| 11 | Feb 4 |
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. The dates for the exams will be announced in time on this website.
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.
- 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