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

空间控制技术与应用 ›› 2008, Vol. 34 ›› Issue (2): 29-32.

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

北京控制工程研究所

出版日期:2008-04-25 发布日期:2021-12-11

Research on ROBDD Variables Reordering Algorithm in Formal Verification

Beijing institute of Control Engineering

Online:2008-04-25 Published:2021-12-11

摘要/Abstract

摘要：

不良的ROBDD变量排序会引发状态空间爆炸的危机, 从而影响形式验证方法的推广和使用。通过对CUDD数据包中ROBDD遗传变量排序算法的研究, 利用变异操作和保留最优个体的时代繁殖操作对原算法进行了改进。实验数据表明, 改进后的算法在可以容忍的运行时间内减少了ROBDD的节点数目, 在一定程度上缓解了形式验证中状态空间爆炸的危机。

关键词: font-family:宋体, ">ROBDD ">ROBDD sfield=kw&, skey=ROBDD&, code=&, ')">uid=WEEvREcwSlJHSldTTEYzVDhUQ01wZWNBc3JTenlNbHhvcDE3MXFEZWxwQT0=$9A4hF_YAuvQ5obgVAqNKPCYcEjKensW4IQMovwHtwkF4VYPoHbKxJw!!" target="https://kns.cnki.net/KXReader/_blank">, font-family:Calibri, sans-serif, ">color:windowtext, 变量排序 ">变量排序 sfield=kw&, skey=%E5%8F%98%E9%87%8F%E6%8E%92%E5%BA%8F&, code=&, ')">uid=WEEvREcwSlJHSldTTEYzVDhUQ01wZWNBc3JTenlNbHhvcDE3MXFEZWxwQT0=$9A4hF_YAuvQ5obgVAqNKPCYcEjKensW4IQMovwHtwkF4VYPoHbKxJw!!" target="https://kns.cnki.net/KXReader/_blank">, color:windowtext, 遗传算法">遗传算法')">">

Abstract: 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.

Key words: font-family:Calibri, sans-serif, ">color:windowtext, ROBDD')">">ROBDD, variables reordering, genetic algorithm, ')">">

中图分类号:

V446

王青, 杨孟飞. 形式验证中ROBDD变量排序算法的研究[J]. 空间控制技术与应用, 2008, 34(2): 29-32.

WANG Qing, YANG Mengfei.

Research on ROBDD Variables Reordering Algorithm in Formal Verification [J]. Aerospace Contrd and Application, 2008, 34(2): 29-32.