IMT'16: Probabilistic model checking with PRISM

The site contains various resources for the Probabilistic Model Checking with PRISM course taught at IMT, Lucca (May 2016).

Slides for the lectures given by Marta Kwiatkowska:
- part 1 (Introduction + Discrete-time Markov chains);
- part 2 (Markov decision processes + strategy synthesis);
- part 3 (LTL verification + new developments in PRISM).
A lab session based on the PRISM tool.

The following papers are recommended background reading:
- for Markov chains see this tutorial paper;
- for Markov decision processes see this tutorial paper;
- for stochastic games see this paper and this tool paper;
- for probabilistic timed automata see this tutorial paper.
The book Principles of of Model Checking by Christel Baier and Joost-Pieter Katoen is recommended reading for the course.
There are further tutorial papers listed here.