Lectures - ESSLLI'10
The following are slides for a lecture course on Probabilistic Model Checking
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
developed also by
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)
Lecture 2 - Markov decision processes (MDPs)
Lecture 3 - Continuous-time Markov chains (CTMCs)
Lecture 4 - Probabilistic model checking in practice
Lecture 5 - Probabilistic timed automata (PTAs)