[KNPS08] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston. Verification of Real-Time Probabilistic Systems. In S. Merz and N. Navet (editors), Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pages 249-288, 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.]
Downloads:  pdf pdf (658 KB)  bib bib
Front cover 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 finite-state 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 finite-state construction in each of the following four sections.