一种改进的区域自动机构造方法

用时间自动机验证一个有穷状态实时系统的正确性，可归结为判定两个时间正则语言的包含问题，亦可归结为判定两个时间正则语言的交是否为空的问题。在判定一个时间正则语言是否为空时，先要将时间自动机转化为无时间的区域自动机。Alur和Dill给出的构造区域自动机的算法，存在许多不可达或虽可达但无用的状态。通过对时钟约束进行分析，在求时钟区域和时间后继的过程中，不断地将一些不可达或无用状态筛掉，使构造出的区域自动机更为优化，改进了Alur等人给出的算法。

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.