# Probabilistic Model Checking: 2016-2017

| |

| Schedule C1 (CS&P) — Computer Science and Philosophy Schedule C1 — Computer Science |

| Michaelmas Term 2016 (20 lectures) |

Please note that the information about course delivery will be updated in accordance to current guidance nearer the start of Michaelmas Term.

## Overview

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.## Learning outcomes

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.

## Prerequisites

No prior knowledge of probability will be assumed.

## Synopsis

- 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

## Syllabus

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.

## Reading list

- Stochastic Model Checking, Marta Kwiatkowska, Gethin Norman and David Parker.
- Automated Verification Techniques for Probabilistic Systems, Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman and David Parker.
- Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press.

(in particular, Chapter 10) - The PRISM user manual

## Related research

| |

| PRISM | Probabilistic Model Checking | Quantitative Analysis and Verification |