[KNPS08]
Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston.
Verification of RealTime Probabilistic Systems.
In S. Merz and N. Navet (editors), Modeling and Verification of RealTime Systems: Formalisms and Software Tools, pages 249288, John Wiley & Sons.
January 2008.
[pdf]
[bib]
http://www.iste.co.uk/index.php?p=a&ACTION=View&id=195
[Tutorial on probabilistic timed automata (PTAs) and the methods used by PRISM to analyse them.]

Available from:
http://www.iste.co.uk/index.php?p=a&ACTION=View&id=195

Abstract.
In this section, we consider a number of automatic verification methods for probabilistic timed automata.
The underlying semantics of a probabilistic timed automaton is generally presented with respect
to the time domain of the real numbers,
and hence the resulting semantic timed Markov decision process
generally has an uncountable number of states and transitions.
Therefore, the methods that we present are based on the construction of finitestate Markov decision processes,
which are defined so that their analysis can be used to infer reachability probabilities
and other performance measures of probabilistic timed automata.
We present a different finitestate construction in each of the following four sections.
