Probabilistic Model Checking and Applications

Learning objectives

In this course we are going to learn the basic principles of probabilistic model checking, a well-established technique for the verification/analysis of probabilistic models. The course will contain an introductory part on stochastic processes (Discrete/Continuous Time Markov chains) as well
as an introductory part on probabilistic temporal logics (PCTL, CSL), i.e. the formal languages for specifying properties of stochastic models which probabilistic model checking is based upon.
The course will then present the algorithms for verifying temporal logic properties against probabilistic models.
The course will contain also a number of tutorials where the students will be asked to develop complete models and to analyse by means of
standard probabilistic model checking tools such as the PRISM model checker. The analysis of standard communication protocols such as, for example the IEEE 802.11 family of distributed coordination functions will be proposed as a case-study to the participants.