基于KQML的多Agent系統(tǒng)建模與驗證.pdf

1、多Agent系統(tǒng)可以看作是多個獨立自主的Agent通過相互通信、交互以及協(xié)作對同一個問題進行求解的分布式智能系統(tǒng)。由于通信的單個Agent具有動態(tài)性和自主性，如何保證多Agent系統(tǒng)的正確性及有效性便成了現(xiàn)階段一大挑戰(zhàn)。由此，形式化分析與驗證多Agent系統(tǒng)越來越成為研究熱點。
　　為了提高多Agent系統(tǒng)的自動化驗證程度，支持時態(tài)、認(rèn)知及合作等性質(zhì)的驗證，本文提出將描述多Agent系統(tǒng)通信語言KQML轉(zhuǎn)化到符號模型檢測工具MCM

2、AS的輸入語言ISPL的一系列轉(zhuǎn)化算法。最后在MCMAS環(huán)境下對火車控制系統(tǒng)和虛擬旅行系統(tǒng)進行形式化建模和驗證，證明本文所提算法的正確性及有效性。本文主要研究以下幾個方面：
　　(1)本文分析并研究了KQML行為原語的關(guān)鍵字及語義，同時考慮符號模型檢測工具MCMAS的輸入語言ISPL的特點，提出了便于KQML語言轉(zhuǎn)化為MCMAS輸入語言ISPL的的中間轉(zhuǎn)化模型——狀態(tài)遷移七元組，為實現(xiàn)多Agent系統(tǒng)的自動化驗證打下基礎(chǔ)。

3、　　(2)將KQML行為原語與能夠反映系統(tǒng)狀態(tài)遷移關(guān)系的遷移七元組一一映射，提出其轉(zhuǎn)化算法K2T，從而實現(xiàn)KQML向形式化模型的自動轉(zhuǎn)化。
　　(3)提出了遷移七元組自動生成MCMAS輸入語言ISPL的轉(zhuǎn)化算法T2I。該算法根據(jù)中間形式化模型狀態(tài)遷移七元組的本身特性及解釋系統(tǒng)建模語言ISPL的特性，實現(xiàn)了遷移七元組到ISPL的自動轉(zhuǎn)化，減少了轉(zhuǎn)化過程中的人工操作。
　　(4)運用符號模型檢測工具MCMAS對火車控制系統(tǒng)及虛擬