This section of the website contains teaching material
covering much of the underlying theory behind PRISM.
There are several sets of lecture slides available:
"Probabilistic model checking"
a 20-lecture course with detailed coverage of model checking
for DTMCs, CTMCs and MDPs
a 5-part course covering some additional topics (e.g. PTAs) but in slightly less depth.
an 11-part course covering some additional topics (e.g. PTAs, case studies) but in slightly less depth.
a 3-part tutorial, with a particular focus on probabilistic hybrid systems.
Citations included in these slides (and other talks on this site)
refer to keys in this list of references.