EFSM最小可达图的同步生成算法  

A Synchro-Generation Algorithm for Reachable Minimal Graph of EFSM

作　　者：眭永波[1] 王忠民[1] 郝瑞兵[1] 

机构地区：[1]北京科技大学计算机科学与技术系,北京100083

出　　处：《计算机工程与应用》2004年第23期80-85,88,共7页Computer Engineering and Applications

基　　金：贝尔实验室中国基础科学研究院(BLRC)资助

摘　　要：针对EFSM可达性分析过程中的状态空间爆炸问题,提出了一种基于变量值域划分的EFSM最小可达图的同步生成算法。该算法将EFSM可达图的生成与最小化两个过程结合在一起同步进行,引入特征配置的思想,依据特征配置指出变迁有效性组合,以及变迁的赋值动作与终止状态分组变量值域的关系,在进行可达性分析的同时仅对可达的状态分组进行稳定性判定及必要的分裂,直到所有可达状态分组均稳定为止,EFSM最小可达图即构造完毕。文中算法最大限度地减小了中间结果如不可达分组等对求解过程的影响,从而降低了传统算法因可达性分析与最小化过程相分离而引起的时间与空间上的巨大代价。The well-known state explosion problem is a great challenge to deriving the minimal reachable graph of EFSM.Here an online minimization algorithm based on the division of variables' value domain is presented to avoid the above harassment.To get it,the two procedures:Reachability Analysis and Minimization,are performed simultaneously.By introducing the Eigen Configuration,only the reachable states are dealt with during the whole process.According to the combination of the outgoing transitions' validity to the eigen configuration,and the correlation between their action and the variables' value domain of the end state,the stability of each reachable state is evaluated,and the necessary splitting is executed on the unstable one at the same time.The algorithm terminates till all reachable states are stable,with the minimal reachable graph achieved.Through the above integration of the two procedures,the influence of many interim results such as the unreachable states is minimized.Hence higher performance than traditional algorithms can be gained.

关 键 词：扩展有限状态机 最小可达图 可达性分析 EFSM 协议测试 变量值域 状态分裂思想 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]