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

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