[KNP04a]
Jan Rutten, Marta Kwiatkowska, Gethin Norman and David Parker.
Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems.
Volume 23 of CRM Monograph Series. American Mathematical Society. P. Panangaden and F. van Breugel (eds.).
March 2004.
[bib]

Abstract.
Probability features increasingly often in software and hardware
systems: it is used in distributed coordination and routing
problems, to model faulttolerance and performance, and to provide
adaptive resource management strategies. Probabilistic model
checking is an automatic procedure for establishing if a desired
property holds in a probabilistic model, aimed at verifying
probabilistic specifications such as "leader election is
eventually resolved with probability 1", "the chance of shutdown
occurring is at most 0.01%", and "the probability that a
message will be delivered within 30ms is at least 0.75". A
probabilistic model checker calculates the probability of a
given temporal logic property being satisfied, as opposed to
validity. In contrast to conventional model checkers, which rely
on reachability analysis of the underlying transition system
graph, probabilistic model checking additionally involves
numerical solutions of linear equations and linear programming problems.
These lecture notes summarise both the theory and the practical details of
automatic verification of probabilistic systems against temporal logic specifications.
We cover discrete and continuoustime Markov chains, Markov decision processes and probabilistic timed automata,
as well as the temporal logics PCTL, CSL and PTCTL.
The usefulness of the techniques is demonstrated through a number of case studies
analysing realworld probabilistic protocols performed with
PRISM,
a probabilistic model checker developed at the University of Birmingham.
