L. Aceto, A. Burgueno, and K. G. Larsen, “Model Checking via Reachability Testing for Timed Automata”, BRICS, vol. 4, no. 29, Jan. 1997.