UPPAAL PRO is an extension of UPPAAL [BDL04], which supports probabilistic reachability for probabilistic timed automata.