Aceto, Luca, et al. “Characteristic Formulae for Timed Automata”. BRICS Report Series, vol. 7, no. 23, Jan. 2000, doi:10.7146/brics.v7i23.20150.