二元判断图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对某篇论文的分析进行了验证,指出并更正了其错误。

【相似文献】

中国期刊全文数据库

前20条

1

钟绍春，刘大有;时态逼近关系及时态逻辑的扩充[J];软件学报;1996年02期

2

张广泉;反应式系统的并发模型(Ⅳ)——时态逻辑模型[J];重庆师范学院学报(自然科学版);1998年04期

3

张广泉,孙敏;时态逻辑的比较与分析[J];渝州大学学报(自然科学版);1999年02期

4

胡金柱,舒忠梅;基于代数-时态逻辑的象形对象研究[J];小型微型计算机系统;2002年06期

5

袁成祥;高济;林东豪;;基于时态逻辑的虚拟企业活动规划[J];计算机科学;2002年02期

6

赖贤伟;胡山立;宁正元;王秀丽;;交互时态逻辑下的三种模糊信念算子[J];海南师范大学学报(自然科学版);2008年04期

7

王秀丽;宁正元;胡山立;赖贤伟;;模糊交互时态逻辑及其语义结构[J];广西师范大学学报(自然科学版);2008年01期

8

白金山;李祥;;具有自反性质的线序时态逻辑研究[J];计算机工程与设计;2011年04期

9

刘清;建立在时态逻辑公式演绎基础上的程序设计[J];计算机应用与软件;1989年01期

10

张骏林;李江宏;;用于协议描述及验证的时态逻辑[J];计算机应用与软件;1992年02期

11

贲可荣,陈火旺,王兵山;命题时态逻辑矢列式演算系统[J];中国科学(A辑 数学 物理学 天文学 技术科学);1994年10期

12

贲可荣，陈火旺;命题时态逻辑定理证明新方法[J];软件学报;1994年07期

13

杜慧敏,韩俊刚,高德远;用于描述和验证数字电路的一阶间隔时态逻辑[J];西北工业大学学报;1999年01期

14

黎升洪;缪淮扣;;时态逻辑描述能力比较研究[J];计算机工程与应用;2006年22期

15

杨秋伟;洪帆;杨木祥;;基于时态逻辑的自动信任协商模型[J];计算机应用研究;2007年11期

16

周巢尘;程序推理[J];计算机应用与软件;1984年02期

17

田国会，刘长有，徐心和;分拣系统运行过程的时态逻辑描述与分析[J];计算机集成制造系统-CIMS;1997年04期

18

宋悦,郝克刚,葛玮;基于时态逻辑的抽象对象规约方法[J];西北大学学报(自然科学版);1999年06期

19

郭建,杜惠敏,韩俊刚,郝克刚;基于时态逻辑的硬件设计形式化验证技术——模型检验[J];小型微型计算机系统;2001年05期

20

杨惠珍,康凤举,马裕民,蔡斌;基于时态逻辑的形式化联邦校核方法[J];西北工业大学学报;2005年04期

中国重要会议论文全文数据库

前5条

1

田国会;刘长有;徐心和;;离散事件动态系统理论的时态逻辑研究方法[A];1996中国控制与决策学术年会论文集[C];1996年

2

田国会;刘长有;徐心和;;电梯服务系统的时态逻辑描述、分析与控制[A];1996年中国控制会议论文集[C];1996年

3

陈玉泉;陈宣;陆汝占;;内涵时态逻辑的语义解释系统[A];自然语言理解与机器翻译——全国第六届计算语言学联合学术会议论文集[C];2001年

4

李晓鸥;郭令忠;徐心和;;Petri网监控的时态逻辑框架[A];1994中国控制与决策学术年会论文集[C];1994年

5

刘新;邹丽;;直觉模糊时态逻辑[A];模糊集理论与应用——98年中国模糊数学与模糊系统委员会第九届年会论文选集[C];1998年

中国博士学位论文全文数据库

前1条

中国硕士学位论文全文数据库

前7条

1

刘冬宁;时态逻辑及其对知识库的构架与研究[D];广东工业大学;2004年

2

李岚;略论时态逻辑在计算机科学中的发展[D];华东师范大学;2013年

3

李学军;基于时态逻辑的迁移实例运行时安全研究[D];山东大学;2009年

5

7