Probabilistic Model Checking: 2009-2010
Lecturer | |
Degrees | Schedule C1 — Computer Science |
Term | Michaelmas Term 2009 (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 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
- 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.
Related research
Themes | |
Activities | PRISM | Probabilistic Model Checking | Quantitative Analysis and Verification |
Taking our courses
This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses
Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.