F. Laroussinie, K. G. Larsen, and C. Weise, “From Timed Automata to Logic - and Back”, BRICS, vol. 2, no. 2, Jan. 1995.