Étienne André, J. Sproston, and L. Fribourg, “An Extension of the Inverse Method to Probabilistic Timed Automata”, ECEASST, vol. 23, Dec. 2009.