Probabilistic Model Checking: 2021-2022
MT21 - The lectures for this course are pre-recorded; they will be released throughout the term on the "Course Materials" page. Please check out slides deck for updated details and possible errata.
Lectures will be supported by discussions during office hours and via the relevant Teams group: please sign up on Minerva for that and for classes/practicals.
Overview of the course - 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, nor of formal verification. A relevant course students might want to consider is the more basic 'Computer-Aided Formal Verification', which is offered concurrently in MT.
- 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
Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.