An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata