形式验证中ROBDD变量排序算法的研究  

Research on ROBDD Variables Reordering Algorithm in Formal Verification

作　　者：王青[1] 杨孟飞[2] 

机构地区：[1]北京控制工程研究所,北京100190 [2]中国空间技术研究院,北京100081

出　　处：《空间控制技术与应用》2008年第2期29-32,共4页Aerospace Control and Application

摘　　要：不良的ROBDD变量排序会引发状态空间爆炸的危机,从而影响形式验证方法的推广和使用。通过对CUDD数据包中ROBDD遗传变量排序算法的研究,利用变异操作和保留最优个体的时代繁殖操作对原算法进行了改进。实验数据表明,改进后的算法在可以容忍的运行时间内减少了ROBDD的节点数目,在一定程度上缓解了形式验证中状态空间爆炸的危机。The ill order of ROBDD variables may cause the crisis of state space explosion and,therefore, influence the use of the formal verification method. In this paper, we present an improved algoribhm by adding mutation and optimized evolution operations to the genetic ROBDD variables reordering algorithm in the CUDD package. The experimental results demonstrate that the proposed algorithm can reduce the number of ROBDD nodes within a tolerable time, and slow down the crisis of state space explosion in the formal verification.

关 键 词：ROBDD 变量排序 遗传算法 

分 类 号：V446[航空宇航科学与技术—飞行器设计]