形式验证中ROBDD变量排序算法的研究
不良的ROBDD变量排序会引发状态空间爆炸的危机,从而影响形式验证方法的推广和使用.通过对CUDD数据包中ROBDD遗传变量排序算法的研究.利用变异操作和保留最优个体的时代繁殖操作对原算法进行了改进.实验数据表明,改进后的算法在可以容忍的运行时间内减少了ROBDD的节点数目,在一定程度上缓解了形式验证中状态空间爆炸的危机.
杨孟飞,YANG Mengfei(中国空间技术研究院,北京,100081)
刊 名： 空间控制技术与应用 英文刊名： AEROSPACE CONTROL AND APPLICATION 年，卷(期)： 2008 34(2) 分类号： V446 关键词： ROBDD 变量排序 遗传算法