Lectures - Probabilistic Model Checking
The following are slides for a lecture course on Probabilistic Model Checking
as taught by Dave Parker
in the Department of Computer Science
at Oxford University.
The course closely follows material from Chapter 10 of
"Principles of Model Checking"
by Christel Baier and Joost-Pieter Katoen (MIT Press) and
"Stochastic Model Checking"
by Marta Kwiatkowska, Gethin Norman and David Parker.
It is an extended version of (a subset of)
this course from ESSLLI'10
and this course from BISS'07.
The tutorial for the
probabilistic model checker PRISM
provides a suitable accompanying practical course.
-
Lecture 1 - Introduction
(slides)
-
Lecture 2 - Discrete-time Markov chains
(slides)
-
Lecture 3 - Discrete-time Markov chains
(slides)
-
Lecture 4 - Probabilistic temporal logics
(slides)
-
Lecture 5 - PCTL model checking for DTMCs
(slides)
-
Lecture 6 - PRISM
(slides)
-
Lecture 7 - Cost and rewards
(slides)
-
Lecture 8 - Continuous-time Markov chains
(slides)
-
Lecture 9 - Continuous-time Markov chains
(slides)
-
Lecture 10 - Model checking CTMCs
(slides)
-
Lecture 11 - Counterexamples & bisimulation
(slides)
-
Lecture 12 - Markov decision processes
(slides)
-
Lecture 13 - Reachability in MDPs
(slides)
-
Lecture 14 - Model checking MDPs
(slides)
-
Lecture 15 - Long-run properties of DTMCs and MDPs
(slides)
-
Lecture 16 - Automata-based properties
(slides)
-
Lecture 17 - ω-regular properties
(slides)
-
Lecture 18 - LTL model checking for DTMCs and MDPs
(slides)
-
Lecture 19 - Probabilistic symbolic model checking
(slides)
All citations from the slides can be found in this list of references
and (where appropriate) the keys match those from the PRISM bibliography.
