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

摘要

针对一种结合最大接受前驱的on-the-fly并行空性检测方法,在接受环最大接受前驱处于环外的情境,无法通过传播接受前驱以on-the-fly方式识别接受环的问题,提出一种传播最大和最新接受前驱的on-the-fly并行空性检测方法.在首次遍历积自动机时,它采用最大接受前驱和最新接受前驱的双值传播模式,最大接受前驱仍保留原方法的传播特征,引入的最新接受前驱追踪并行空性检测的局部遍历特征,使其在原方法传播接受前驱识别失效时仍能on-the-fly识别接受环.理论证明了该算法的正确性,对比实验验证了该算法提前终止率更高,时空成本更低,on-the-fly优势更强.在软件模型检测领域,该方法为并行空性检测进一步控制状态空间爆炸,提供了一种有效途径.