Probabilistic Model Checking: 20142015
Lecturer 

Degrees 
Schedule C1 — Computer Science 
Term 
Michaelmas Term 2014 (20 lectures) 
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 stateofthe art probabilistic checking tool PRISM, based here in Oxford). The methods used will be illustrated through a variety of reallife 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
 Discretetime 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
 Continuoustime Markov chains (CTMCs)
 Model checking for CTMCs
 Implementation and data structures: symbolic techniques
Syllabus
Introduction to probabilistic model checking; probabilistic models: discretetime Markov chains, Markov decision processes, continuoustime 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 JoostPieter Katoen, MIT Press.
(in particular, Chapter 10)  The PRISM user manual
Related research at the Department of Computer Science
Themes 

Activities 
PRISM  Probabilistic Model Checking  Quantitative Analysis and Verification 