  There has been a growing interest in defining models of automata enriched
with time, such as finite automata extended with clocks (timed automata). In
this paper, we study deterministic timed finite state machines (TFSMs), i.e.,
finite state machines with a single clock, timed guards and timeouts which
transduce timed input words into timed output words. We solve the problem of
equivalence checking by defining a bisimulation from timed FSMs to untimed ones
and viceversa. Moreover, we apply these bisimulation relations to build the
intersection of two timed finite state machines by untiming them, intersecting
them and transforming back to the timed intersection.
