L. Aceto, A. Burgueno, og K. G. Larsen, “Model Checking via Reachability Testing for Timed Automata”, BRICS, bd. 4, nr. 29, jan. 1997.