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''.