Characteristic formulae for timed automata. - Luca Aceto; Anna Ingólfsdóttir; Mikkel Lykke Pedersen; Jan Poulsen (RAIRO Theor. Informatics Appl., 2000)