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.