基于OBDD的SMC中PRE(E)操作的改进算法

• 作者: 姚全珠 魏小勇
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 排序二值判定图 符号模型检测 PRE(操作 深度优先搜索
• 年，卷（期）: 2008,（14）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 69-71,74
• 页数: 4页
• 分类号: TP311
• 字数: 4909字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2008.14.025

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	姚全珠	西安理工大学计算机科学与工程学院	84	918	15.0	26.0
2	魏小勇	西安理工大学计算机科学与工程学院	1	4	1.0	1.0