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.