Probabilistic Model Checking: 2020-2021
The lectures for this course will be pre-recorded.
They will be released throughout the term on the "Course Materials" page.
They will be supported by discussion via the Teams group - please sing up on Minerva and stay tuned.
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.
No prior knowledge of probability will be assumed.
- 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
- 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.
- 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