Oxford logo
[KNS00] M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability. Technical report CSR-00-01, University of Birmingham, School of Computer Science. January 2000. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (140 KB)  pdf pdf (303 KB)  bib bib
Abstract. We consider probabilistic timed automata of [13], an extension of the timed automata model of [2] with discrete probability distributions. In contrast to timed automata, which model real-time systems purely in terms of nondeterminism, our model allows to express the likelihood of the system making certain transitions, and is thus appropriate for modelling fault-tolerance and probabilistic failures. We present a symbolic model checking algorithm for the existential fragment of the logic PTCTL of [13] based on backward reachability as in [12]. The logic allows us to specify properties such as ``with probability 0.99 or greater, it is possible to correctly deliver a data packet within 5 time units'', or ``with probability 0.87 or greater, the system never enters an error state''.