Lectures

The following are slides for a lecture course on probabilistic model checking.

This materially was originally used for a 15-hour course at the BISS 2007 school in March 2007.

• Part 1: Introduction
  (introduction to probabilistic model checking)
  
  
• Part 2: Discrete-time Markov chains (DTMCs)
  (introduction to DTMCs and PCTL, model checking algorithms, examples)
• Part 3: DTMC case studies
  (Bluetooth device discovery, contract signing)
  
  
• Part 4: Markov decision processes (MDPs)
  (introduction to MDPs and PCTL, model checking algorithms, examples)
  
  
• Part 5: Continuous-time Markov chains (CTMCs)
  (introduction to CTMCs and CSL, model checking algorithms, examples)
• Part 6: CTMC case studies
  (dynamic power management, biological systems)
  
  
• Part 7: Probabilistic timed automata (PTAs)
  (introduction to PTAs and PTCTL, model checking algorithms, examples)
• Part 8: PTA case studies
  (FireWire root contention, CSMA/CD)
  
  
• Part 9: The PRISM tool
  (tool support, PRISM: functionality, resources, modelling language, properties)
  (see also the PRISM Tutorial)
• Part 10: Implementation of probabilistic model checking
  (implementation overview, symbolic techniques: BDDs and MTBDDs)
• Part 11: Advanced topics
  (parallelisation, approximate verification, research areas)

All citations from the slides can be found in this list of references and (where appropriate) the keys match those from the PRISM bibliography.