二元判斷圖BDD及其JAVA實(shí)現(xiàn)的應(yīng)用與研究

【摘要】：

在數(shù)字控制系統(tǒng)、計(jì)算機(jī)輔助設(shè)計(jì)(CAD),計(jì)算機(jī)輔助測(cè)試(CAT)、人工智能(AI)以及可編程控制器等領(lǐng)域的許多問(wèn)題都可以表示成一系列關(guān)于布爾函數(shù)的運(yùn)算,這些運(yùn)算有賴于布爾函數(shù)的符號(hào)表示和算法的有效性。一般而言,我們通常采用布爾函數(shù)表達(dá)式或真值表來(lái)描述數(shù)字邏輯函數(shù)。布爾函數(shù)是一種可以精確地描述數(shù)字邏輯函數(shù)的方法。

但隨著大規(guī)模和超大規(guī)模集成電路的迅速發(fā)展,數(shù)字邏輯函數(shù)的運(yùn)算變得日益復(fù)雜,上述的傳統(tǒng)方法逐漸暴露出一些缺點(diǎn),比如使用布爾函數(shù)來(lái)表示數(shù)字邏輯函數(shù)的話,表達(dá)式往往會(huì)變得龐大和復(fù)雜,使得函數(shù)處理時(shí)間過(guò)長(zhǎng);而使用真值表方式的話,則需要占用大量的存儲(chǔ)空間,只能用在一些特殊的領(lǐng)域。鑒于上述的情況,研究人員不斷的探索,試圖找到描述更加簡(jiǎn)潔、操作更加方便的數(shù)字邏輯函數(shù)表達(dá)方式。

1986年,E.R.Bryant提出了用二元判斷圖BDD(Binary Decision Diagram)來(lái)表示布爾函數(shù),和其他表示法相比BDD在人們尋找大型數(shù)字系統(tǒng)的有效分析、測(cè)試和計(jì)算方法中,由于其固有的優(yōu)越性能而日益受到重視。綜合來(lái)說(shuō),BDD具有如下的優(yōu)點(diǎn):

(1)直觀,明了,便于邏輯電路的分析。

(2)能反映數(shù)字電路的邏輯描述的細(xì)節(jié),這點(diǎn)對(duì)電路的分析和測(cè)試非常重要。

(3)便于計(jì)算機(jī)的存儲(chǔ),編寫(xiě)的程序比布爾代數(shù)方法編寫(xiě)的程序更短。

(4)便于使用人工智能的方法,啟發(fā)式進(jìn)行求解空間搜索。

(5)不管是硬件還是軟件實(shí)現(xiàn),都能獲得比布爾代數(shù)算法更高的執(zhí)行速度。

(6)可應(yīng)用并行圖論算法,進(jìn)一步提高運(yùn)算速度。

模型檢測(cè)主要是驗(yàn)證某一模型生成的有限狀態(tài)系統(tǒng)是否滿足模型所要求的屬性。模型檢測(cè)技術(shù)可以抽象地描述為:給定一個(gè)模型M和邏輯描述的性質(zhì)P,檢查模型M中性質(zhì)P是否成立。模型檢測(cè)主要是驗(yàn)證某一模型生成的有限狀態(tài)系統(tǒng)是否滿足模型所要求的屬性。模型檢測(cè)中最大的挑戰(zhàn)就是狀態(tài)空間的爆炸問(wèn)題。這個(gè)問(wèn)題源于系統(tǒng)中有許多不同部件的交互,或者系統(tǒng)中有取值范圍很大的復(fù)雜數(shù)據(jù)結(jié)構(gòu),在這種情況下系統(tǒng)狀態(tài)的規(guī)模將變得非常龐大。由于BDD所用的存儲(chǔ)空間較少,因此研究人員將BDD引入到了模型檢驗(yàn)中,使得模型檢驗(yàn)所能驗(yàn)證的系統(tǒng)規(guī)模得到了很大的提高。

時(shí)態(tài)邏輯在模型檢測(cè)中占有非常重要的地位,模型檢測(cè)是基于時(shí)態(tài)邏輯,時(shí)態(tài)邏輯的模型可能由幾個(gè)狀態(tài)構(gòu)成,時(shí)態(tài)邏輯公式可能在一些狀態(tài)為真,在其它為假,因此,該公式的值隨著狀態(tài)的變化而變化。依據(jù)對(duì)系統(tǒng)狀態(tài)的時(shí)間路徑的不同刻畫(huà),時(shí)態(tài)邏輯可以分成兩大類:計(jì)算樹(shù)時(shí)態(tài)邏輯(CTL)和線性時(shí)態(tài)邏輯(LTL)。

CTL是由Clarke和Emerson提出的。它的運(yùn)算符具有簡(jiǎn)單的性質(zhì),可以有效地計(jì)算某一公式在有窮狀態(tài)模型處于某一狀態(tài)時(shí)是否滿足。它是一種時(shí)間模型采用樹(shù)的方式、具有多個(gè)分支的不確定狀態(tài)路徑構(gòu)成。

在模型檢測(cè)過(guò)程中采用BDD的主要原因是:采用BDD表達(dá)的兩個(gè)謂詞公式時(shí),兩個(gè)BDD范式邏輯相等當(dāng)且僅當(dāng)這兩個(gè)BDD范式是語(yǔ)法相等,即兩個(gè)BDD范式邏輯相等,當(dāng)且僅當(dāng)這兩個(gè)BDD范式是同一個(gè)BDD范式。目前,利用BDD來(lái)對(duì)規(guī)劃問(wèn)題求解的基本思想是:先將規(guī)劃問(wèn)題的狀態(tài)和動(dòng)作表示為BDD范式,再將其輸入到BDD的求解器,然后將求解得到的結(jié)果轉(zhuǎn)化為一般規(guī)劃問(wèn)題的表示。

JAVABDD是一套非常優(yōu)秀的用于BDD的生成,執(zhí)行各種邏輯操作,描述狀態(tài)變化的Java開(kāi)源軟件包?？梢岳锰总浖_(kāi)發(fā)出CTL的各種公式,實(shí)現(xiàn)簡(jiǎn)單的模型檢測(cè)功能。

本文所做主要工作如下:

1.為了能夠有效地使用和擴(kuò)充JavaBDD這套軟件,我們對(duì)該軟件的主要算法進(jìn)行了代碼分析。包括:

(1) MK算法和Build算法:JavaBDD是如何將數(shù)組的存儲(chǔ)效率和哈希表的查找效率有效地結(jié)合起來(lái),從而建立ROBDD的數(shù)據(jù)結(jié)構(gòu),使其占空間少,查找速度快.

(2) APPLY算法:JavaBDD是如何實(shí)現(xiàn)兩個(gè)布爾表達(dá)式之間的邏輯操作。

(3) RESTRIC算法,JavaBDD如何計(jì)算布爾表達(dá)式的賦值結(jié)果

(4) SATCOUNT算法:計(jì)算ROBDD中的可滿足集元素個(gè)數(shù)。

(5) ANYSAT算法:尋找一個(gè)可滿足的賦值。

(6) ALLSAY算法:尋找全部可滿足賦值。

(7) JavaBDD中存在量詞,全稱量詞與唯一量詞的算法實(shí)現(xiàn)。

2.為JavaBDD增加了差集運(yùn)算功能。

3.將皇后問(wèn)題轉(zhuǎn)化為邏輯操作,利用JavaBDD計(jì)算結(jié)果。

4.利用JavaBDD進(jìn)行電路電路功能分析與等價(jià)性判斷。

5.利用JavaBDD實(shí)現(xiàn)計(jì)算樹(shù)時(shí)序邏輯的AX,EX,AF,EF,AG,EG,AU,EU操作符。

6.利用JavaBDD完成Mlner's Soheduder例子,演示了有限狀態(tài)轉(zhuǎn)移與求可達(dá)狀態(tài)集的例子。

7.利用我們編制的CTL對(duì)某篇論文的分析進(jìn)行了驗(yàn)證,指出并更正了其錯(cuò)誤。

【相似文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù)

前20條

1

鐘紹春，劉大有;時(shí)態(tài)逼近關(guān)系及時(shí)態(tài)邏輯的擴(kuò)充[J];軟件學(xué)報(bào);1996年02期

2

張廣泉;反應(yīng)式系統(tǒng)的并發(fā)模型(Ⅳ)——時(shí)態(tài)邏輯模型[J];重慶師范學(xué)院學(xué)報(bào)(自然科學(xué)版);1998年04期

3

張廣泉,孫敏;時(shí)態(tài)邏輯的比較與分析[J];渝州大學(xué)學(xué)報(bào)(自然科學(xué)版);1999年02期

4

胡金柱,舒忠梅;基于代數(shù)-時(shí)態(tài)邏輯的象形對(duì)象研究[J];小型微型計(jì)算機(jī)系統(tǒng);2002年06期

5

袁成祥;高濟(jì);林東豪;;基于時(shí)態(tài)邏輯的虛擬企業(yè)活動(dòng)規(guī)劃[J];計(jì)算機(jī)科學(xué);2002年02期

6

賴賢偉;胡山立;寧正元;王秀麗;;交互時(shí)態(tài)邏輯下的三種模糊信念算子[J];海南師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年04期

7

王秀麗;寧正元;胡山立;賴賢偉;;模糊交互時(shí)態(tài)邏輯及其語(yǔ)義結(jié)構(gòu)[J];廣西師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年01期

8

白金山;李祥;;具有自反性質(zhì)的線序時(shí)態(tài)邏輯研究[J];計(jì)算機(jī)工程與設(shè)計(jì);2011年04期

9

劉清;建立在時(shí)態(tài)邏輯公式演繹基礎(chǔ)上的程序設(shè)計(jì)[J];計(jì)算機(jī)應(yīng)用與軟件;1989年01期

10

張駿林;李江宏;;用于協(xié)議描述及驗(yàn)證的時(shí)態(tài)邏輯[J];計(jì)算機(jī)應(yīng)用與軟件;1992年02期

11

賁可榮,陳火旺,王兵山;命題時(shí)態(tài)邏輯矢列式演算系統(tǒng)[J];中國(guó)科學(xué)(A輯 數(shù)學(xué) 物理學(xué) 天文學(xué) 技術(shù)科學(xué));1994年10期

12

賁可榮，陳火旺;命題時(shí)態(tài)邏輯定理證明新方法[J];軟件學(xué)報(bào);1994年07期

13

杜慧敏,韓俊剛,高德遠(yuǎn);用于描述和驗(yàn)證數(shù)字電路的一階間隔時(shí)態(tài)邏輯[J];西北工業(yè)大學(xué)學(xué)報(bào);1999年01期

14

黎升洪;繆淮扣;;時(shí)態(tài)邏輯描述能力比較研究[J];計(jì)算機(jī)工程與應(yīng)用;2006年22期

15

楊秋偉;洪帆;楊木祥;;基于時(shí)態(tài)邏輯的自動(dòng)信任協(xié)商模型[J];計(jì)算機(jī)應(yīng)用研究;2007年11期

16

周巢塵;程序推理[J];計(jì)算機(jī)應(yīng)用與軟件;1984年02期

17

田國(guó)會(huì)，劉長(zhǎng)有，徐心和;分揀系統(tǒng)運(yùn)行過(guò)程的時(shí)態(tài)邏輯描述與分析[J];計(jì)算機(jī)集成制造系統(tǒng)-CIMS;1997年04期

18

宋悅,郝克剛,葛瑋;基于時(shí)態(tài)邏輯的抽象對(duì)象規(guī)約方法[J];西北大學(xué)學(xué)報(bào)(自然科學(xué)版);1999年06期

19

郭建,杜惠敏,韓俊剛,郝克剛;基于時(shí)態(tài)邏輯的硬件設(shè)計(jì)形式化驗(yàn)證技術(shù)——模型檢驗(yàn)[J];小型微型計(jì)算機(jī)系統(tǒng);2001年05期

20

楊惠珍,康鳳舉,馬裕民,蔡斌;基于時(shí)態(tài)邏輯的形式化聯(lián)邦校核方法[J];西北工業(yè)大學(xué)學(xué)報(bào);2005年04期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù)

前5條

1

田國(guó)會(huì);劉長(zhǎng)有;徐心和;;離散事件動(dòng)態(tài)系統(tǒng)理論的時(shí)態(tài)邏輯研究方法[A];1996中國(guó)控制與決策學(xué)術(shù)年會(huì)論文集[C];1996年

2

田國(guó)會(huì);劉長(zhǎng)有;徐心和;;電梯服務(wù)系統(tǒng)的時(shí)態(tài)邏輯描述、分析與控制[A];1996年中國(guó)控制會(huì)議論文集[C];1996年

3

陳玉泉;陳宣;陸汝占;;內(nèi)涵時(shí)態(tài)邏輯的語(yǔ)義解釋系統(tǒng)[A];自然語(yǔ)言理解與機(jī)器翻譯——全國(guó)第六屆計(jì)算語(yǔ)言學(xué)聯(lián)合學(xué)術(shù)會(huì)議論文集[C];2001年

4

李曉鷗;郭令忠;徐心和;;Petri網(wǎng)監(jiān)控的時(shí)態(tài)邏輯框架[A];1994中國(guó)控制與決策學(xué)術(shù)年會(huì)論文集[C];1994年

5

劉新;鄒麗;;直覺(jué)模糊時(shí)態(tài)邏輯[A];模糊集理論與應(yīng)用——98年中國(guó)模糊數(shù)學(xué)與模糊系統(tǒng)委員會(huì)第九屆年會(huì)論文選集[C];1998年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù)

前1條

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù)

前7條

1

劉冬寧;時(shí)態(tài)邏輯及其對(duì)知識(shí)庫(kù)的構(gòu)架與研究[D];廣東工業(yè)大學(xué);2004年

2

李嵐;略論時(shí)態(tài)邏輯在計(jì)算機(jī)科學(xué)中的發(fā)展[D];華東師范大學(xué);2013年

3

李學(xué)軍;基于時(shí)態(tài)邏輯的遷移實(shí)例運(yùn)行時(shí)安全研究[D];山東大學(xué);2009年

5

7

總結(jié)

以上是生活随笔為你收集整理的bdd java_二元判断图BDD及其JAVA实现的应用与研究的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。