二元判斷圖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

總結

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

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。