Skip to main content

Probabilistic Model Checking:  2014-2015



Schedule C1Computer Science

Schedule C1Mathematics and Computer Science

Schedule CMSc in Computer Science



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.


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
  • Counterexamples
  • 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.

Reading list

Related research at the Department of Computer Science