传播最大和最新接受前驱的On-the-Fly并行空性检测  

Parallel Emptiness Check Propagating Maximal and Newly Discovered Accepting Predecessors

作　　者：赵璐 张健沛[2] 杨静[2] 

机构地区：[1]天津城建大学计算机与信息工程学院,天津300384 [2]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001

出　　处：《小型微型计算机系统》2015年第6期1203-1208,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61370083;61073043;61073041)资助;高等学校博士学科点专项科研基金项目(20112304110011;20122304110012)资助;哈尔滨市科技创新人才研究专项资金项目(2011RFXXG015)资助

摘　　要：针对一种结合最大接受前驱的on-the-fly并行空性检测方法,在接受环最大接受前驱处于环外的情境,无法通过传播接受前驱以on-the-fly方式识别接受环的问题,提出一种传播最大和最新接受前驱的on-the-fly并行空性检测方法.在首次遍历积自动机时,它采用最大接受前驱和最新接受前驱的双值传播模式,最大接受前驱仍保留原方法的传播特征,引入的最新接受前驱追踪并行空性检测的局部遍历特征,使其在原方法传播接受前驱识别失效时仍能on-the-fly识别接受环.理论证明了该算法的正确性,对比实验验证了该算法提前终止率更高,时空成本更低,on-the-fly优势更强.在软件模型检测领域,该方法为并行空性检测进一步控制状态空间爆炸,提供了一种有效途径.For an on-the-fly parallel emptiness check with map （maximum accepting predecessor） ,there is a scenario where no accep- ting cycle is on-the-fly identified by its map propagation,i, e. map is out of the cycle. To solve the problem,a parallel emptiness check propagating maximal and newly discovered accepting predecessors is presented. In initial traversal phase of the state space of a product automaton,the proposed method propagates the map and nap （ newly discovered accepting predecessor） values simultaneously. The map value is the same as the counterpart of the original method,and the nap value tracks the local traversal characteristic of the parallel emptiness check. Under the above scenario, the proposed method could discover an accepting cycle using nap propagation. The correct- ness of this method is theoretically proved. Comparison experiments show that our method has higher early termination ratio, lower cost of time and memory, and more on-the-flyness than the original method. In the domain of software model checking, this method gives an effective way for parallel emptiness check to further alleviate the state-space explosion.

关 键 词：软件模型检测 并行空性检测 Biichi自动机 on—the-fly方法 

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