Probabilistic Model Checking:

Literature

Hans Hansson, Bengt Jonsson:
A Logic for Reasoning about Time and Reliability

Marta Kwiatkowska, Gethin Norman and David Parker:
Quantitative analysis with the probabilistic model checker PRISM.

B. Jeannet, P.R. D'Argenio, and K.G. Larsen:
RAPTURE: A tool for verifying Markov Decision Processes

Tools

PRISM (Birmingham; analysis of DTMC, CTMC and MDP wrt PCTL)

RAPTURE (IRISA, Twente, Aalborg; analysis of DTMC, MDP wrt probabilistic reachability)