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

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