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.

Background reading