期刊文献+
共找到60篇文章
< 1 2 3 >
每页显示 20 50 100
带有互补边的共享OBDDs及数据结构
1
作者 孟礼 武小悦 《计算机工程与科学》 CSCD 北大核心 2013年第1期180-184,共5页
顺序二元决策图OBDDs的规模随着变量数量的增多呈指数形式增长。为了克服大规模OBDDs数据的描述和存储困难,提出了一种带有互补边的共享OBDDs的数据结构,并定义了一组OBDDs节点的关键属性,该数据结构融合了共享OBDDs和带有互补边的OBDD... 顺序二元决策图OBDDs的规模随着变量数量的增多呈指数形式增长。为了克服大规模OBDDs数据的描述和存储困难,提出了一种带有互补边的共享OBDDs的数据结构,并定义了一组OBDDs节点的关键属性,该数据结构融合了共享OBDDs和带有互补边的OBDDs的特点。最后通过存储空间实例对比分析,证明了该数据结构能够有效描述和存储大规模OBDDs数据。 展开更多
关键词 大规模obdds 共享obdds 互补边 数据结构
下载PDF
Probabilistic Verification over GF(2m) Using Mod2-OBDDs
2
作者 J.L. Imana 《Intelligent Information Management》 2010年第2期95-103,共9页
Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean cir... Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean circuit specifications and logic designs, but these methods require a large amount of memory and time. Due to these limitations, several models of Decision Diagrams have been studied and other verification techniques have been proposed. In this paper, we have used probabilistic verification with Galois (or finite) field GF(2m) modifying the CUDD package for the computation of signatures in classical OBDDs, and for the construction of Mod2-OBDDs (also known as ?-OBDDs). Mod2-OBDDs have been constructed with a two-level layer of ?-nodes using a positive Davio expansion (pDE) for a given variable. The sizes of the Mod2-OBDDs obtained with our method are lower than the Mod2-OBDDs sizes obtained with other similar methods. 展开更多
关键词 VERIFICATION PROBABILISTIC OBDD Mod2-OBDD GALOIS FIELD GF(2m)
下载PDF
Short-Time Scaling of Variable Orderingof OBDDs 被引量:1
3
作者 龙望宁 闵应骅 +1 位作者 杨士元 童诗白 《Journal of Computer Science & Technology》 SCIE EI CSCD 1997年第4期366-371,共6页
A short-time scaling criterion of variable ordering of OBDDs is proposed. By this criterion it is easy and fast to determine which one is better when several. variable orders are given, especially when they differ 10%... A short-time scaling criterion of variable ordering of OBDDs is proposed. By this criterion it is easy and fast to determine which one is better when several. variable orders are given, especially when they differ 10% or more in resulted BDD size from each other. An adaptive variable order selection method, based on the short-time scaling criterion, is also presented. The experimental results show that this method is efficient and it makes the heuristic variable ordering methods more practical. 展开更多
关键词 Boolean function logical verification ordered binary decision diagram (OBDD) OBDD variable ordering.
原文传递
Efficient Heuristic Variable Ordering of OBDDs
4
作者 龙望宁 闵应骅 +2 位作者 边计年 杨士元 薛宏熙 《Tsinghua Science and Technology》 EI CAS 2000年第2期211-216,共6页
An efficient heuristic algorithm for variable ordering of OBDDs, the WDHA (Weight and Distance based Heuristic Algorithm), is presented. The algorithm is based on the heuristics implied in the circuit structure grap... An efficient heuristic algorithm for variable ordering of OBDDs, the WDHA (Weight and Distance based Heuristic Algorithm), is presented. The algorithm is based on the heuristics implied in the circuit structure graph. To scale the heuristics, pi -weight , node -weight , average -weight and pi -distance in the circuit structure graph are defined. As any of the heuristics is not a panacea for all circuits, several sub algorithms are proposed to cope with various cases. One is a direct method that uses pi -weight and pi -distance . The others are based on the depth first search (DFS) traversal of the circuit structure graph, with each focusing on one of the heuristics. An adaptive order selection strategy is adopted in WDHA. Experimental results show that WDHA is efficient in terms of BDD size and run time, and the dynamic OBDD variable ordering is more attractive if combined with WDHA. 展开更多
关键词 binary decision diagram Boolean function OBDD variable ordering logic verification
原文传递
多智能体系统时态认知规范高效符号模型检测的算法研究 被引量:2
5
作者 吴立军 苏金树 苏开乐 《计算机学报》 EI CSCD 北大核心 2008年第2期245-252,共8页
Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领... Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展,然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法. 展开更多
关键词 obdds mu演算 时态认知逻辑 符号模型检测 安全协议验证
下载PDF
无圈与或图搜索的符号OBDD算法研究
6
作者 王雪松 赵岭忠 古天龙 《计算机科学》 CSCD 北大核心 2010年第7期169-173,共5页
与或图搜索是人工智能领域一项重要的问题求解技术。基于传统数据结构的与或图表示技术极大地限制了与或图搜索算法可求解问题的规模。在无圈与或图符号OBDD表示的基础上,给出了一种求解无圈与或图最小代价解图的符号搜索算法。实验结... 与或图搜索是人工智能领域一项重要的问题求解技术。基于传统数据结构的与或图表示技术极大地限制了与或图搜索算法可求解问题的规模。在无圈与或图符号OBDD表示的基础上,给出了一种求解无圈与或图最小代价解图的符号搜索算法。实验结果表明,与AO*算法相比,该算法可处理问题的规模有较大的提高。 展开更多
关键词 与或图 最小代价解图 obdds
下载PDF
电力系统低压减载和低频减载协调控制策略 被引量:28
7
作者 佘庆媛 沈沉 +1 位作者 乔颖 谭伟 《电力系统自动化》 EI CSCD 北大核心 2008年第23期23-27,共5页
低压减载和低频减载是分别解决电力系统中电压稳定问题和频率稳定问题的最常用手段。实际系统中,电压稳定问题和频率稳定问题往往是互相耦合、共同存在的,单独采用一种策略难以同时解决2个问题。文中提出了一种可以实现低压减载和低频... 低压减载和低频减载是分别解决电力系统中电压稳定问题和频率稳定问题的最常用手段。实际系统中,电压稳定问题和频率稳定问题往往是互相耦合、共同存在的,单独采用一种策略难以同时解决2个问题。文中提出了一种可以实现低压减载和低频减载协调控制的方法。该方法将切负荷控制中的优化问题转化成一个可满足性校验问题,然后采用"搜索+校验"的思路进行求解。求解过程中先采用有序二元决策图(OBDD)等快速搜索算法缩小决策空间,然后针对其中的策略进行可满足性校验。该方法不用求解复杂的多目标、混合整数优化问题,直接得到可行的切负荷策略。最后给出了基于此方法的仿真算例,并通过时域暂态仿真验证了结果的准确性。 展开更多
关键词 电力系统 低压减载 低频减载 有序二元决策图(OBDD)
下载PDF
OBDD变量排序的自适应选择算法 被引量:8
8
作者 贝劲松 边计年 +2 位作者 薛宏熙 龙望宁 洪先龙 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 1999年第5期412-416,共5页
有序的二叉决策图(OBDD)是形式验证领域的基础技术之一.由于OBDD的大小对变量序非常敏感,使得变量排序问题成为最关键的一个问题.首先将OBDD变量排序问题分解为3 个子问题,定义了若干启发信息,给出了上述子问题的... 有序的二叉决策图(OBDD)是形式验证领域的基础技术之一.由于OBDD的大小对变量序非常敏感,使得变量排序问题成为最关键的一个问题.首先将OBDD变量排序问题分解为3 个子问题,定义了若干启发信息,给出了上述子问题的启发式解法;然后提出了一个变量排序自适应选择算法,从若干候选变量序中选出“最佳”的变量序.最后给出了ISCAS85 电路的实验结果. 展开更多
关键词 布尔函数 OBDD 组合电路 形式验证 集成电路
下载PDF
OBDD在组合逻辑电路测试中的应用研究 被引量:7
9
作者 吕宗伟 林争辉 张镭 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2001年第6期495-499,共5页
传统的组合逻辑电路测试方法在搜索过程中都不可避免地要进行反向回溯 ,由于反向回溯的次数过多 ,往往会降低算法的效率 .文中利用 OBDD来表示电路中每个节点所代表的逻辑函数 ,把传统算法中的反向回溯过程转换为 OBDD图的问题 ,从而加... 传统的组合逻辑电路测试方法在搜索过程中都不可避免地要进行反向回溯 ,由于反向回溯的次数过多 ,往往会降低算法的效率 .文中利用 OBDD来表示电路中每个节点所代表的逻辑函数 ,把传统算法中的反向回溯过程转换为 OBDD图的问题 ,从而加快了故障测试的速度 .同时 。 展开更多
关键词 组合逻辑电路 故障检测 OBDD 测试 逻辑函数
下载PDF
一种求解认知难题的模型检测方法 被引量:5
10
作者 骆翔宇 苏开乐 顾明 《计算机学报》 EI CSCD 北大核心 2010年第3期406-414,共9页
用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以... 用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以验证相关的时态认知性质,这一特性是当前认知逻辑模型检测工具MCK、MCMAS和DEMO不能完全支持的.作者采用OBDD开发了相关的符号化模型检测工具MCTK并对和与积难题进行建模和验证,实验结果说明了文中方法的正确性和高效性. 展开更多
关键词 模型检测 OBDD 公告逻辑 时态认知逻辑 和与积难题
下载PDF
基于重量分析的OBDD变量排序算法 被引量:6
11
作者 龙望宁 杨士元 +1 位作者 闵应骅 童诗白 《计算机学报》 EI CSCD 北大核心 1997年第8期702-710,共9页
有序的二叉判决图(OBDD)是布尔表达式的一种有效表示方法,但它的体积对变量排序具有较强的依赖性.本文提出一种电路结构图,并在此基础上定义了原始输入重量和节点重量等参数,并建立了用重量分析来指导的OBDD变量排序算法... 有序的二叉判决图(OBDD)是布尔表达式的一种有效表示方法,但它的体积对变量排序具有较强的依赖性.本文提出一种电路结构图,并在此基础上定义了原始输入重量和节点重量等参数,并建立了用重量分析来指导的OBDD变量排序算法.由于从考虑变量对输出函数的影响出发与从考虑OBDD节点共享性出发对变量排序的要求不同,本文分别设计了两类算法.实验结果表明,本文对大多数标准电路变量排序的效果都优于国际上的同类算法,尤其是对一些较难排序的电路(如C2670)效果更加突出. 展开更多
关键词 二叉判决图 OBDD 变量排序 逻辑设计 计算机
下载PDF
约束满足问题求解的符号OBDD桶消元算法 被引量:4
12
作者 徐周波 古天龙 +1 位作者 常亮 李凤英 《计算机科学》 CSCD 北大核心 2011年第7期200-202,219,共4页
桶消元算法是求解约束满足问题的一种典型推理方法。针对桶消元算法面临的状态空间爆炸问题,将有序二叉决策图(OBDD)技术与该算法结合起来,给出了约束满足问题的一种求解算法。通过对约束满足问题中变量和域值的编码,将CSP问题转化为命... 桶消元算法是求解约束满足问题的一种典型推理方法。针对桶消元算法面临的状态空间爆炸问题,将有序二叉决策图(OBDD)技术与该算法结合起来,给出了约束满足问题的一种求解算法。通过对约束满足问题中变量和域值的编码,将CSP问题转化为命题可满足性问题,给出了约束满足问题的OBDD表示方法;基于桶消元的算法思想,在约束满足问题的OBDD表示的基础上,利用OBDD的"与"操作和"量化"操作等,避免了传统算法中状态的显式枚举,隐式地实现了对CSP的求解。对大量随机生成的测试用例进行了实验分析,结果表明提出的符号算法明显优于桶消元法和符号直接求解法。 展开更多
关键词 约束满足问题 符号算法 桶消元 有序二叉决策图(OBDD)
下载PDF
大型工程项目施工系统可靠性评估 被引量:3
13
作者 杨莉琼 李世蓉 徐波 《重庆大学学报(社会科学版)》 CSSCI 北大核心 2012年第5期64-69,共6页
施工系统的可靠性评估有助于减少项目风险、优化工程目标。文章综合考虑项目质量、成本、时间和安全目标,提出基于有序二元决策图(OBDD)的施工系统可靠性评估方法。该方法便于计算机实现,具有很高的计算效率,适合大型工程项目。最后,通... 施工系统的可靠性评估有助于减少项目风险、优化工程目标。文章综合考虑项目质量、成本、时间和安全目标,提出基于有序二元决策图(OBDD)的施工系统可靠性评估方法。该方法便于计算机实现,具有很高的计算效率,适合大型工程项目。最后,通过算例演示了施工系统可靠性的评估过程,并验证了该方法。 展开更多
关键词 大型工程项目 施工系统 可靠性评估 OBDD
下载PDF
异步时序电路分析的一种OBDD方法 被引量:2
14
作者 吕毅 姚志江 +1 位作者 魏道政 解永良 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2001年第6期500-504,共5页
对异步时序电路的分析和使用是一个比较困难的问题 ,所以 ,异步时序电路的实际应用范围远不如同步时序电路 .通过改进 JR Burch等提出的分析方法 ,使之适用于异步时序电路 .该方法使用基于 OBDD的布尔特征函数来表示电路的转移关系 ,并... 对异步时序电路的分析和使用是一个比较困难的问题 ,所以 ,异步时序电路的实际应用范围远不如同步时序电路 .通过改进 JR Burch等提出的分析方法 ,使之适用于异步时序电路 .该方法使用基于 OBDD的布尔特征函数来表示电路的转移关系 ,并通过基于 OBDD的布尔函数的运算来确定异步时序电路的稳定状态、及当输入改变时电路的下一个稳定状态 。 展开更多
关键词 异步时序电路 特征函数 有序二元判决图 OBDD
下载PDF
装配几何可行性判别的符号OBDD技术研究 被引量:1
15
作者 钟艳如 梁永强 +1 位作者 黄美发 古天龙 《计算机工程与应用》 CSCD 北大核心 2007年第3期50-53,共4页
采用了有序二叉决策图(OBDD)描述装配几何可行性,给出了装配操作及其几何可行性的符号表示,设计了装配操作几何可行性的符号OBDD判别算法,给出了装配几何可行性的研究实例,开发了装配的原型系统以支持装配规划,原型系统运行结果表明符号... 采用了有序二叉决策图(OBDD)描述装配几何可行性,给出了装配操作及其几何可行性的符号表示,设计了装配操作几何可行性的符号OBDD判别算法,给出了装配几何可行性的研究实例,开发了装配的原型系统以支持装配规划,原型系统运行结果表明符号OBDD技术用于装配几何可行性判别的有效性。 展开更多
关键词 装配操作 OBDD 几何可行性
下载PDF
“离散数学”中的OBDD案例教学研究 被引量:5
16
作者 徐周波 古天龙 《计算机教育》 2010年第2期122-124,共3页
"离散数学"是计算机专业的核心课程,是研究计算机科学的数学理论基础。有序二叉决策图(OBDD-Ordered Binary Decision Diagram)是描述布尔函数的一种新的有效的数据结构。文章提出在课本知识的讲授过程中,引入OBDD来解析离散... "离散数学"是计算机专业的核心课程,是研究计算机科学的数学理论基础。有序二叉决策图(OBDD-Ordered Binary Decision Diagram)是描述布尔函数的一种新的有效的数据结构。文章提出在课本知识的讲授过程中,引入OBDD来解析离散数学在计算机专业其他学科中的具体应用,加深学生对所学知识点的理解,并激发学生的学习兴趣和创新能力,从而引导学生充分认识离散数学在计算机专业中的重要作用。这对于提高"离散数学"课程的教学水平和质量,以及学生对后续课程的学习和今后进一步的科学研究均具有现实意义。 展开更多
关键词 离散数学 OBDD 数据结构 教学
下载PDF
用OBDD算法评估无线传感网的可靠度和结点重要性 被引量:1
17
作者 肖宇峰 陈山枝 +1 位作者 李昕 李玉宏 《高技术通讯》 EI CAS CSCD 北大核心 2009年第12期1245-1250,共6页
基于有序二叉判定图(OBDD),提出用结点扩张(NE)算法来评估无线传感网的可靠度和结点重要性。NE算法执行结点扩张操作来处理不可靠结点,从两方面增强了计算效率:利用OBDD结构表示网络状态,减少了大量冗余的等价状态;利用Hash表存储同构... 基于有序二叉判定图(OBDD),提出用结点扩张(NE)算法来评估无线传感网的可靠度和结点重要性。NE算法执行结点扩张操作来处理不可靠结点,从两方面增强了计算效率:利用OBDD结构表示网络状态,减少了大量冗余的等价状态;利用Hash表存储同构子网的OBDD,减少了同构子网的重复计算。另外,该算法对结点重要性进行了评估,为脆弱结点的保护提供参考。实验结果表明NE算法的计算开销比传统的factoring算法低,能有效评估无线传感网的可靠度。 展开更多
关键词 无线传感网 网络可靠度 有序二叉判定图(OBDD) 因子分解
下载PDF
PSL的有界模型检验 被引量:2
18
作者 虞蕾 赵宗涛 《电子学报》 EI CAS CSCD 北大核心 2009年第3期614-621,共8页
基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性... 基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程. 展开更多
关键词 PSL(property specification language) 有界模型检验(bounded model checking BMC) SAT(propositional satisfiability) OBDD(ordered binary decision diagram)
下载PDF
一类Petri网调度问题的符号求解技术 被引量:2
19
作者 古天龙 李风英 《系统仿真学报》 CAS CSCD 北大核心 2005年第z1期148-150,154,共4页
讨论了Petri网分析的符号有序二叉决策图(Ordered Binary Decision Disgram--OBDD)技术.对于一类赋时Petri网模型的生产调度问题,通过实施赋时位置(迁移)结构等价替换,建立了调度问题求解的符号算法.该算法可以在makespan步得到结果,从... 讨论了Petri网分析的符号有序二叉决策图(Ordered Binary Decision Disgram--OBDD)技术.对于一类赋时Petri网模型的生产调度问题,通过实施赋时位置(迁移)结构等价替换,建立了调度问题求解的符号算法.该算法可以在makespan步得到结果,从而有效改善了求解的效率,适合于复杂大规模Petri网模型调度问题的求解. 展开更多
关键词 PETRI网 有序二叉决策图(OBDD) 调度 可达性 离散事件系统
下载PDF
一种新的基于OBDD的装配序列推理方法 被引量:2
20
作者 刘华东 古天龙 《桂林电子科技大学学报》 2006年第6期464-468,共5页
根据机械装配序列推理的特点,对PADL-2提供的CAD模型数据进行简化处理,再结合有序二叉决策图(OBDD-O rdered B inary D ec is ion D iagram),建立了一种新的装配体模型。基于此模型,可以通过一系列的OBDD符号运算完成装配操作的可行性判... 根据机械装配序列推理的特点,对PADL-2提供的CAD模型数据进行简化处理,再结合有序二叉决策图(OBDD-O rdered B inary D ec is ion D iagram),建立了一种新的装配体模型。基于此模型,可以通过一系列的OBDD符号运算完成装配操作的可行性判断,从而实现了装配序列的推理。这种推理方法容易实现计算机化和自动化,是对文献[6]中推理方法的一种改进。通过对实例的实现和分析证明了该方法是切实可行的。 展开更多
关键词 装配序列 OBDD 接触函数 装配序列推理
下载PDF
上一页 1 2 3 下一页 到第
使用帮助 返回顶部