基于时间自动机的符号状态拆分优化算法

摘要

为约简时间自动机的状态空间,对时间抽象互模拟技术进行研究,提出一种改进的符号状态拆分算法.通过在符号状态拆分的过程中将隐含的时钟约束加入符号状态来缩小符号状态的时间域,减少符号状态拆分的次数,提高符号状态拆分算法的效率.为实现符号状态拆分算法,提出一种改进的DBM(difference bound matrices)减法算法.将减法算法得到非凸多面体用互不重叠DBM集合来表示,使得由符号状态拆分算法得到的等价类中没有冗余的等价类.实验结果表明了改进后的符号状态拆分算法和DBM减法的有效性.%To reduce the state space of timed automata,time-abstracting bisimulations technology was studied.An improvement of symbol state splitting algorithm was proposed.The time domain of the symbolic state was reduced by adding the implicit time constraint to the symbolic state in the process of symbol state splitting.The time domain of the symbolic state was reduced which reduced the number of symbolic states to be split and improved the efficiency of symbol state splitting algorithm.To rea-lize the symbol state splitting algorithm,an improvement of DBM (difference bound matrices) subtraction algorithm was proposed.A non-convex polyhedron resulted from the subtraction was represented by non-overlapping DBMs set.Improved DBM subtraction algorithm makes the results of the symbol state splitting algorithm do not contain redundant equivalence classes.Experimental results show that the improved symbol state splitting algorithm and the DBM subtraction algorithm are effective.