Probabilistic Model Checking in Practice

This tutorial will cover some of the practical aspects of probabilistic model checking. In particular, it will focus on the use of PRISM, a widely used tool for verification of discrete-time Markov chains, continuous-time Markov chains, Markov decision processes and extensions of these models with costs and rewards. The tutorial will cover PRISM's modelling and property specification languages and give an overview of its underlying techniques. It will also offer hands-on experience with the tool itself.