L. Aceto, A. Ingólfsdóttir, M. L. Pedersen, and J. Poulsen, “Characteristic Formulae for Timed Automata”, BRICS, vol. 7, no. 23, Jan. 2000.