A simplification of the untiming procedure for timed automata
Michael R. Laurence, Michael P. Spathopoulos · 2002
Given a timed automaton G accepting the language L/sup T/, a finite state machine G' can be constructed, known as the region automaton, which accepts the untimed language ut(L/sup T/). We construct an alternative finite state machine which also accepts the language ut(L/sup 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.