Kim G. Larsen:
Probabilistic
Models, Logics and Equivalences
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
PRISM (Birmingham; analysis of DTMC, CTMC and MDP wrt PCTL)
RAPTURE (IRISA, Twente, Aalborg; analysis of DTMC, MDP wrt probabilistic reachability)