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

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

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