Real-time automata
We study here the class of timed
automata
with a single clock which is reset at each transition. We adapt for
these
automata the classical results for finite automata: the Kleene
theorem, the closure under complementation and the Pumping Lemma. We
provide an
algorithm for the elimination of stuttering steps, which is essential
in
complementation. This algorithm relies upon the properties of the Kleene algebra of sets of real numbers, namely
the
existence of a normal form for sets of reals
generated from intervals with rational bounds, using boolean operations,
summation and star.
“Journal of Automata, Languages and Combinatorics”, vol.6, no.1, pages 3-23, 2001.