Advances in Probabilistic Model Checking
The site contains various resources for the summer-school:
-
Slides for the lectures given by Marta Kwiatkowska:
- part 1 (introduction + discrete-time Markov chains);
- part 2 (Markov decision processes);
- part 3 (compositional probabilistic verification);
- part 4 (probabilistic timed automata).
-
A reference list
for papers on probabilistic model checking, as cited in the lecture slides
There are also accompanying exercises:
For the written exercises, you may find the following resources helpful:
- this more in-depth lecture course
- this tutorial chapter: [KNP07a] (for discrete-time Markov chains)
- this tutorial chapter: [FKNP11] (for Markov decision processes)
