www.prismmodelchecker.org

KTH'15: Probabilistic verification and synthesis

PRISM Lab Session

To practice the material taught in the lectures you should attempt exercises here for Markov chains and here for Markov decision processes.

This hands-on tool session will introduce you to PRISM. To get started, download and install it. It is best to make sure that you are running the latest version (currently 4.3), but any version from 4.1 onwards should be fine.

This lab session is self-contained, but if you want information about running PRISM the best source is the online manual.

There are three parts, of which Parts A and B are of standard difficulty, and Part C is considered advanced:

  • Part A uses a simple discrete-time Markov chain (DTMC) example - a randomised algorithm for modelling a 6-sided die with a fair coin. It introduces the basics of the PRISM modelling language and the PRISM tool.

  • Part B is an example of a self-stabilisation protocol that uses both DTMCs.

  • Part C is based on a dynamic power management system, and illustrates how to build PRISM models comprising multiple interacting components. It uses both DTMCs and MDPs.

If you want to learn about other aspects of PRISM, take a look at the main online tutorial.

You can also find many more interesting examples in the case studies section of the website.

Documentation