A simplification of the untiming procedure for timed automata defining languages of finite strings

Given an Alur Timed Automaton G accepting the language L^T, as defined in [1], a finite state machine G can be constructed, which accepts the language Untime(L^T). G is known as the region automaton. Here we construct an alternative finite state machine G* that also accepts the language Untime(L^T), but has significantly fewer states than G. The new untiming procedure involves finite timed words only.