On An Algebraic Definition of Timed Regular Languages
We prove that the class of timed languages accepted by finite automata, in the sense of Eilenberg, does not include any language with ``quantitative'' timing. That is, once a signal is accepted by a finite automaton, any other signal with the same ``untimed trace'' is accepted too. The proof makes use of the notion of automaton over a monoid, and is based upon a lemma showing that any nontrivial morphism from the monoid of nonnegative real numbers to a finite monoid maps all positive reals into a ``zero'' of the finite monoid.
“Proceedings of 2nd Romanian-Austrian Workshop on Computer-Aided Verification of Information Systems”, Timisoara, Romania, 2004.