Probabilistic Model Checking

The lecturer will not be assuming any prior knowledge of probability.

Probabilistic model checking is a formal technique for analysing systems that exhibit probabilistic behaviour. Examples include randomised algorithms, communication and security protocols, computer networks, biological signalling pathways, and many others. The course provides a detailed introduction to these techniques, covering both the underlying theory (Markov chains, Markov decision processes, temporal logics) and its practical application (using the state-of-the art probabilistic checking tool PRISM, based here in Oxford). The methods used will be illustrated through a variety of real-life case studies, e.g. the Bluetooth/FireWire protocols and algorithms for contract signing and power management.

At the end of the course students are expected to: 

• Understand the theory (models and logics) used in probabilistic model checking;
• Be able to apply the basic algorithms used to perform these techniques;
• Be able to use the software tool PRISM to model and analyse simple probabilistic systems.

• Introduction to probabilistic model checking
• Discrete-time Markov chains (DTMCs) and their properties
• Probabilistic temporal logics: PCTL, LTL, etc.
• The PRISM model checker
• PCTL model checking for DTMCs
• Expected costs and rewards
• Markov decision processes (MDPs)
• PCTL model checking for MDPs
• Counterexamples
• Probabilistic LTL model checking
• Continuous-time Markov chains (CTMCs)
• Model checking for CTMCs
• Implementation and data structures: symbolic techniques

Introduction to probabilistic model checking; probabilistic models: discrete-time Markov chains, Markov decision processes, continuous-time Markov chains; probabilistic temporal logics: PCTL, CSL, LTL; model checking algorithms for PCTL, CSL, LTL; the PRISM model checker; symbolic probabilistic model checking.

• Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press
  (in particular, Chapter 10)
• Stochastic Model Checking, M. Kwiatkowska, G. Norman and D. Parker.
• The PRISM user manual.