L. Aceto, A. Ingólfsdóttir, M. L. Pedersen, og J. Poulsen, “Characteristic Formulae for Timed Automata”, BRICS, bd. 7, nr. 23, jan. 2000.