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

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

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

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

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

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

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

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

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