[KNS03d] M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Model Checking for Probabilistic Timed Automata. Technical report CSR-03-10, School of Computer Science, University of Birmingham. October 2003. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (165 KB)  pdf pdf (395 KB)  bib bib
Notes: This is an extended version of [KNSW04].

Initial experimential results concerning a prototype implemation of the algorithms presented in this paper are available from the PRISM web page.
Abstract. Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We present symbolic model checking algorithms for probabilistic timed automata to verify qualitative properties, corresponding to satisfaction with probability 0 or 1, as well as quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, that is, sets of valuations of the probabilistic timed automaton's clocks, and therefore avoid an explicit construction of the state space. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper completes the symbolic framework for the verification of probabilistic timed automata against full PTCTL. We formulate new algorithms that can return the minimal probability with which a probabilistic timed automaton satisfies a property, thus extending a previously published result concerning the maximum probability.