Abstract: This paper proposes an improved algorithm of PRE operation in Symbolic Model Checking(SMC), and it traverses OBDD B(p1r…pnr.B is a step in PRE operation), and “deletes” all the nodes whose variables (p1r, p2r,…,pnr) are quantified, and gets a non-deterministic OBDD NB that equals p1r…pnr.B, which then is translated into an OBDD Bp1r…pnr. The result shows that it can effectively reduce the time and space of PRE operation.

Key words: Ordered Binary Decision Diagram(OBDD), Symbolic Model Checking(SMC), PRE, operation, Depth-First Search(DFS)

摘要： 提出一种基于排序二值判定图(OBDD)的符号模型检测中PRE操作的改进算法。该算法处理PRE步骤3(嵌套布尔存在量化)的方法是一次遍历“删除”所有被量化变量的节点，产生表示布尔函数与嵌套存在量化结果等价的不确定排序二值判定图，把不确定排序二值判定图转换成OBDD。实验表明，该算法能有效缩短计算时间，减少中间节点所需空间。

关键词: 排序二值判定图, 符号模型检测, PRE, 操作, 深度优先搜索

CLC Number: 

• TP311