AN IMPROVEMENT ON THE CONSTRUCTION OF REGION AUTOMATON

To verify the correctness of the finite state real time system by timed automaton can come down to the inclusion of two timed regular languages. It also boils down to deciding the emptiness of the intersection of two timed regular languages. Timed automaton must be translated into the untimed region automaton at first if the emptiness of a timed automaton is to be decided. Alur and Dill gives an algorithm to construct a region automaton where exist a lot of states which can’t be reached or can be reached but useless. By analyzing the clock constraint one can get rid of reachless or useless states during calculating clock region and time successor. An improved algorithm is presented to construct a region automaton, which is more optimal than Alur’s.