Probabilistic Model Checking: 2010-2011
Information
|
Lecturer |
|
|
Degrees |
Schedule C1 — Computer Science |
|
Term |
Michaelmas Term 2010 (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 at the Department of Computer Science
|
Themes |
|
|
Activities |
PRISM | Probabilistic Model Checking | Quantitative Analysis and Verification |