A simplification of the untiming procedure for timed automata

Given a timed automaton G accepting the language L^T, a finite state machine G´ can be constructed, known as the region automaton, which accepts the untimed language ut(L^T). We construct an alternative finite state machine which also accepts the language ut(L^T), but has fewer states than G´. This is shown for languages of both finite and infinite traces given that the time jump in the transition is strictly positive