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
- 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
The following papers are recommended background reading:
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.