多智能體系統(tǒng)的符號模型檢測.pdf

1、模型檢測作為一種有限狀態(tài)系統(tǒng)的自動化驗證技術已得到廣泛應用。最近該技術在規(guī)劃和多智能體系統(tǒng)(MAS)等人工智能領域的應用也越來越受到重視。MAS領域強調(diào)智能體的自治性和推理力，采用模態(tài)邏輯刻畫智能體心智狀態(tài)(包括智能體的知識、信念、愿望和意圖)的演變過程。由于這些模態(tài)詞的語義解釋與標準時態(tài)算子不同，因此不能直接將當前的LTL或CTL時態(tài)邏輯模型檢測工具應用到多智能體系統(tǒng)中。 本文重點研究多智能體系統(tǒng)的規(guī)范表示及其模型檢測方法。根

2、據(jù)智能體知識、信念、愿望和意圖的表示和建模需求，提出新的Kripke語義模型，并在這一新的語義模型基礎上研究多智能體系統(tǒng)的時態(tài)認知邏輯模型檢測算法。這里提出的時態(tài)認知邏輯是在分支時態(tài)邏輯CTL*語言中加入表示智能體知識、信念、愿望或意圖的認知模態(tài)詞后得到的。該時態(tài)認知邏輯有豐富的時態(tài)和認知表達能力，用戶可以方便地檢測智能體認知狀態(tài)的演變過程。因此，本文研究成果在時態(tài)和認知兩方面擴展并豐富了當前的多智能體系統(tǒng)模型檢測技術。 另一方面，為了

3、大幅緩解模型檢測的狀態(tài)爆炸問題，我們分別采用有序二叉判定圖(OBDD)和 可滿足性(SAT)兩種符號計算技術設計本文的符號模型檢測算法，使得可驗證問題的規(guī)模大大增加。 根據(jù)本文提出的理論，我們已實現(xiàn)兩個高效的符號模型檢測工具MCTK和MCKBDI，其中MCTK用于檢測智能體的知識，而MCKBDI主要用于檢測智能體的信念、愿望和意圖。 本文的研究成果主要體現(xiàn)在以下幾方面： 1. 提出一個時態(tài)邏輯CTL*的符號模型檢測算法。

4、該算法通過tableau構造方法和基于OBDD的不動點計算來判定一個有限狀態(tài)系統(tǒng)是否滿足CTL*規(guī)范。根據(jù)該算法，我們已在符號模型檢測工具NuSMV 2.1.2的基礎上擴展實現(xiàn)一個CTL*符號模型檢測工具MCTK，并完成相當數(shù)量的實驗。到目前為止，有名的符號模型檢測工具，如SMV和NuSMV等，都只能檢測CTL*的子集邏輯(如CTL和LTL)。 2. 通過引入“知道”和“公共知識”等知識模態(tài)詞到時態(tài)邏輯CTL*的語言中，我們得到

5、一個新的時態(tài)知識邏輯CTL*K。根據(jù)帶局部命題的解釋系統(tǒng)語義，提出一個基于OBDD的CTL*K符號模型檢測算法。通過量化智能體的不可觀察變量，CTL*K公式中的知識模態(tài)詞得以消除。該算法已在MCTK基礎上擴展實現(xiàn)，并用MCTK成功驗證若干有名的知識檢測問題。 3. 當前，依賴高度計算復雜性的密碼協(xié)議不斷受到計算機硬件和算法性能提升的沖擊。因此，分析與驗證基于信息論的安全協(xié)議在包含無限計算能力智能體的環(huán)境中的安全性就顯得尤為重要了

6、。我們將本文的時態(tài)知識邏輯模型檢測理論和工具MCTK應用到一類基于信息論的安全協(xié)議驗證中。成功驗證了就餐保密家協(xié)議、Herbivore匿名通信協(xié)議和俄羅斯牌協(xié)議。與著名的同類模型檢測工具MCK和MCMAS相比，MCTK的運行效率占有絕對優(yōu)勢，而且MCTK在協(xié)議建模的易用性上也遠好于MCMAS。這說明我們的理論和工具在工業(yè)級的安全協(xié)議驗證中有很大的應用潛力。 4. 基于SAT的有界模型檢測(BMC)是基于OBDD的符號模型檢測技術

7、的一個重要補充。根據(jù)同步解釋系統(tǒng)語義，提出一個分支時態(tài)知識邏輯ACTL*K (CTL*K的全稱子集邏輯)的有界模型檢測方法。通過引入狀態(tài)位置函數(shù)的方法獲得同步系統(tǒng)的智能體知識，避免了為時間域而擴展通常的時態(tài)認知模型的狀態(tài)及遷移關系編碼。ACTL*K的時態(tài)認知表達能力強于另一個邏輯ACTLK。 5. 提出一個新的關于智能體知識、信念、愿望和意圖的模型，稱為KBDI解釋系統(tǒng)模型(簡稱KBDI模型)。該模型的關鍵概念是將智能體的知識、

8、信念、愿望和意圖分別表示為解釋系統(tǒng)模型中的計算路徑集合。該模型可以很方便地由KBDI智能體編程語言生成。提出KBDI模型的符號模型檢測算法，在MCTK基礎上進一步擴展實現(xiàn)一個多智能體KBDI邏輯的符號模型檢測工具MCKBDI，并獲得一些令人滿意的實驗結果。 多智能體系統(tǒng)模型檢測技術的研究不僅有重要的理論意義，還有重大的實際應用價值。 本文可認為是多智能體邏輯模型檢測的基礎理論和關鍵技術方面的一些階段性成果。多智能體系統(tǒng)的模型檢測