Lectures - ESSLLI'10

The following are slides for a lecture course on Probabilistic Model Checking taught by Marta Kwiatkowska and Dave Parker at the ESSLLI'10 summer-school.

The course comprises five 1.5-hour lectures. You can also find here an extended version of some parts of this course (all except PTAs). The material on PTAs is an updated version of lectures from an earlier tutorial at BISS'07, developed also by Gethin Norman.

The tutorial for the probabilistic model checker PRISM provides a suitable accompanying practical course.

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

• Lecture 1 - Intro + Discrete-time Markov chains (DTMCs) [slides]
• Lecture 2 - Markov decision processes (MDPs) [slides]
• Lecture 3 - Continuous-time Markov chains (CTMCs) [slides]
• Lecture 4 - Probabilistic model checking in practice [slides]
• Lecture 5 - Probabilistic timed automata (PTAs) [slides]

Site hosted at the Department of Computer Science, University of Oxford