Marktoberdorf 2011 Summer-School

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)