计算机工程 ›› 2008, Vol. 34 ›› Issue (14): 69-71.doi: 10.3969/j.issn.1000-3428.2008.14.025

• 软件技术与数据库 • 上一篇    下一篇

基于OBDD的SMC中PRE操作的改进算法

姚全珠,魏小勇   

  1. (西安理工大学计算机科学与工程学院,西安 710048)
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-07-20 发布日期:2008-07-20

Improved Algorithm of PRE Operation in Symbolic Model Checking Based on OBDD

YAO Quan-zhu, WEI Xiao-yong   

  1. (School of Computer Science and Engineering, Xi’an University of Technology, Xi’an 710048)
  • Received:1900-01-01 Revised:1900-01-01 Online:2008-07-20 Published:2008-07-20

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

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

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)

中图分类号: