In this thesis, we focus on the modeling formalism networks of probabilistic timed automata. Networks of probabilistic timed automata may be used to model systems where time, i.e. delays and timeouts, concurrency and synchronisation as well as probabilistic behaviour, either from the system or its environment, are all important properties in the model. We introduce a forward state space exploration and reduction algorithm to partition the state space of probabilistic and normal timed automata according to time-abstract equivalences. We demonstrate how this partitioning can be used to compute probabilistic reachabilities. A prototype tool, Uppaal Prob, has been implemented as an extension to the Uppaal Prob tool. This includes the state space exploration and reduction algorithm, refinement according to probabilistic reachability formulae and computation of maximal reachability probabilities.