时间自动机与自动验证

给出时间自动机的基本概念 ,描述了区域自动机的构造方法 ,并且实现了区域自动机的构造算法 .简述了通过时间自动机进行自动验证的过程 。

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

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