二元判断图BDD及其JAVA实现的应用与研究

论文摘要

在数字控制系统、计算机辅助设计(CAD),计算机辅助测试(CAT)、人工智能(AI)以及可编程控制器等领域的许多问题都可以表示成一系列关于布尔函数的运算,这些运算有赖于布尔函数的符号表示和算法的有效性。一般而言,我们通常采用布尔函数表达式或真值表来描述数字逻辑函数。布尔函数是一种可以精确地描述数字逻辑函数的方法。但随着大规模和超大规模集成电路的迅速发展,数字逻辑函数的运算变得日益复杂,上述的传统方法逐渐暴露出一些缺点,比如使用布尔函数来表示数字逻辑函数的话,表达式往往会变得庞大和复杂,使得函数处理时间过长;而使用真值表方式的话,则需要占用大量的存储空间,只能用在一些特殊的领域。鉴于上述的情况,研究人员不断的探索,试图找到描述更加简洁、操作更加方便的数字逻辑函数表达方式。1986年,E.R.Bryant提出了用二元判断图BDD(Binary Decision Diagram)来表示布尔函数,和其他表示法相比BDD在人们寻找大型数字系统的有效分析、测试和计算方法中,由于其固有的优越性能而日益受到重视。综合来说,BDD具有如下的优点:(1)直观,明了,便于逻辑电路的分析。(2)能反映数字电路的逻辑描述的细节,这点对电路的分析和测试非常重要。(3)便于计算机的存储,编写的程序比布尔代数方法编写的程序更短。(4)便于使用人工智能的方法,启发式进行求解空间搜索。(5)不管是硬件还是软件实现,都能获得比布尔代数算法更高的执行速度。(6)可应用并行图论算法,进一步提高运算速度。模型检测主要是验证某一模型生成的有限状态系统是否满足模型所要求的属性。模型检测技术可以抽象地描述为:给定一个模型M和逻辑描述的性质P,检查模型M中性质P是否成立。模型检测主要是验证某一模型生成的有限状态系统是否满足模型所要求的属性。模型检测中最大的挑战就是状态空间的爆炸问题。这个问题源于系统中有许多不同部件的交互,或者系统中有取值范围很大的复杂数据结构,在这种情况下系统状态的规模将变得非常庞大。由于BDD所用的存储空间较少,因此研究人员将BDD引入到了模型检验中,使得模型检验所能验证的系统规模得到了很大的提高。时态逻辑在模型检测中占有非常重要的地位,模型检测是基于时态逻辑,时态逻辑的模型可能由几个状态构成,时态逻辑公式可能在一些状态为真,在其它为假,因此,该公式的值随着状态的变化而变化。依据对系统状态的时间路径的不同刻画,时态逻辑可以分成两大类:计算树时态逻辑(CTL)和线性时态逻辑(LTL)。CTL是由Clarke和Emerson提出的。它的运算符具有简单的性质,可以有效地计算某一公式在有穷状态模型处于某一状态时是否满足。它是一种时间模型采用树的方式、具有多个分支的不确定状态路径构成。在模型检测过程中采用BDD的主要原因是:采用BDD表达的两个谓词公式时,两个BDD范式逻辑相等当且仅当这两个BDD范式是语法相等,即两个BDD范式逻辑相等,当且仅当这两个BDD范式是同一个BDD范式。目前,利用BDD来对规划问题求解的基本思想是:先将规划问题的状态和动作表示为BDD范式,再将其输入到BDD的求解器,然后将求解得到的结果转化为一般规划问题的表示。JAVABDD是一套非常优秀的用于BDD的生成,执行各种逻辑操作,描述状态变化的Java开源软件包。可以利用套软件包开发出CTL的各种公式,实现简单的模型检测功能。本文所做主要工作如下:1.为了能够有效地使用和扩充JavaBDD这套软件,我们对该软件的主要算法进行了代码分析。包括:(1) MK算法和Build算法:JavaBDD是如何将数组的存储效率和哈希表的查找效率有效地结合起来,从而建立ROBDD的数据结构,使其占空间少,查找速度快.(2) APPLY算法:JavaBDD是如何实现两个布尔表达式之间的逻辑操作。(3) RESTRIC算法,JavaBDD如何计算布尔表达式的赋值结果(4) SATCOUNT算法:计算ROBDD中的可满足集元素个数。(5) ANYSAT算法:寻找一个可满足的赋值。(6) ALLSAY算法:寻找全部可满足赋值。(7) JavaBDD中存在量词,全称量词与唯一量词的算法实现。2.为JavaBDD增加了差集运算功能。3.将皇后问题转化为逻辑操作,利用JavaBDD计算结果。4.利用JavaBDD进行电路电路功能分析与等价性判断。5.利用JavaBDD实现计算树时序逻辑的AX,EX,AF,EF,AG,EG,AU,EU操作符。6.利用JavaBDD完成Mlner’s Soheduder例子,演示了有限状态转移与求可达状态集的例子。7.利用我们编制的CTL对某篇论文的分析进行了验证,指出并更正了其错误。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景
• 1.2 国内外研究状况
• 1.3 JAVABDD简介
• 第二章 BDD的原理与发展
• 2.1 布尔函数与BDD
• 2.1.1 INF操作与香农表达式
• 2.1.2 编序二元判断图ROBDD
• 2.2 ROBDD的构建和操作
• 2.2.1 MK算法
• 2.2.2 JAVABDD中MK算法的实现
• 2.2.3 Build算法
• 2.2.4 APPLY算法
• 2.2.5 JAVABDD中APPLY算法的实现
• 2.2.6 RESTRIC算法
• 2.2.7 JavaBDD中RESTRICT算法的实现
• 2.2.8 SATCOUNT算法
• 2.2.9 ANYSAT算法
• 2.2.10 ALLSAT算法
• 2.2.11 JavaBDD中的路径算法的实现
• 2.2.12 SIMPLIFY算法
• 2.3 BDD与量词逻辑
• 2.3.1 量词逻辑
• 2.3.2 JavaBDD的量词实现
• 2.3.3 BDD中差集的实现
• 2.4 用ROBDD解决问题的例子
• 2.4.1 8皇后问题:
• 2.4.2 逻辑电路的功能分析
• 2.4.3 电路的等价判断
• 第三章 模型检验
• 3.1 验证的建模
• 3.2 计算树逻辑的语法
• 3.3 计算树逻辑的语义
• 3.4 CTL公式间的等价性
• 3.5 CTL验证的例子——进程互斥
• 3.6 模型检验算法
• 3.6.1 标签算法
• 3.6.2 模型检验算法的程序实现
• 3.7 CTL的不动点特性
• 3.7.1 单调函数
• EG的正确性'>3.7.2 SAT_EG的正确性
• EU的正确性'>3.7.3 SAT_EU的正确性
• 3.8 符号模型检验
• 3.8.1 状态集的表示
• 3.8.2 迁移关系的表示
• 第四章 JavaBDD实现CTL
• 4.1 JavaBDD中状态集的表示
• 4.2 JAVABDD实现状态的转化关系及令牌环的演示
• 4.3 利用JavaBDD使现CTL
• 4.3.1 利用JavaBDD求可达状态集
• 4.3.2 利用JavaBDD实现EX
• 4.4 CTL的应用例子
• 4.4.1.同步电路
• 4.4.2 微波炉
• 本文的不足与以后所需进行的工作
• 致谢
• 参考文献