Verification of Probabilistic Systems

This tutorial introduces probabilistic model checking, a formal verification technique for systems that exhibit stochastic behaviour. These methods have been used to analyse a wide range of systems, including communication protocols such as Bluetooth and FireWire, randomised security protocols, e.g. for anonymity and contract signing, and many others. This talk gives an overview of some of the underlying theory of probabilistic model checking, focusing on discrete-time Markov chains and Markov decision processes, the temporal logic PCTL and associated model checking algorithms. These techniques will be illustrated through a selection of real-world case studies.