張 濤，謝 紅，黃少濱

?

多Agent交互策略模型檢測(cè)方法

張 濤1,2，謝 紅2，黃少濱1

(1. 東北農(nóng)業(yè)大學(xué)電氣與信息學(xué)院 哈爾濱 150030；2. 哈爾濱工程大學(xué)信息與通信工程學(xué)院 哈爾濱 150001)

提出一種基于模型檢測(cè)的多Agent交互策略驗(yàn)證方法，首先通過責(zé)任政策語(yǔ)言建模多Agent的交互策略，基于責(zé)任政策語(yǔ)言的操作語(yǔ)義將政策模型轉(zhuǎn)換為模型檢測(cè)器NuSMV的輸入，利用時(shí)態(tài)邏輯聲明表征策略沖突的系統(tǒng)性質(zhì)，然后利用模型檢測(cè)器NuSMV自動(dòng)驗(yàn)證政策模型對(duì)性質(zhì)的可滿足性，并根據(jù)模型檢測(cè)器產(chǎn)生的反例分析交互策略中的各種錯(cuò)誤。該方法可提高交互策略的驗(yàn)證效率，確保多Agent系統(tǒng)設(shè)計(jì)的正確性。

形式化方法; 模型檢測(cè); 多Agent系統(tǒng); NuSMV; 政策建模

多Agent系統(tǒng)中，責(zé)任一般是Agent為了滿足某些要求而執(zhí)行的動(dòng)作[1]，如“社會(huì)保障管理?xiàng)l例規(guī)定企業(yè)在成立之日起的20個(gè)工作日內(nèi)，需持營(yíng)業(yè)執(zhí)照到當(dāng)?shù)厣鐣?huì)保險(xiǎn)經(jīng)辦機(jī)構(gòu)辦理社會(huì)保險(xiǎn)登記”。責(zé)任或是Agent被要求保持的某種狀態(tài)[2]，如“養(yǎng)老保險(xiǎn)繳費(fèi)人員必須處于參保狀態(tài)”。責(zé)任政策約束其所屬領(lǐng)域內(nèi)Agent間的交互行為，可被視為系統(tǒng)設(shè)計(jì)中的高層“需求規(guī)格”或“交互策略”[3]。在多Agent系統(tǒng)中，建模和驗(yàn)證多Agent間的交互策略有助于正確設(shè)計(jì)Agent間的交互行為，提高系統(tǒng)的正確性和可靠性[4]。文獻(xiàn)[5]在計(jì)算機(jī)科學(xué)領(lǐng)域提出研究規(guī)律政策的觀點(diǎn)，文獻(xiàn)[6]開創(chuàng)了關(guān)于分布式系統(tǒng)中的政策研究方向，并提出了“規(guī)律控制的交互(law-governed interaction, LGI)”，由此激發(fā)了該領(lǐng)域的深遠(yuǎn)研究與大量實(shí)踐工作。盡管LGI模型曾被成功用于多Agent系統(tǒng)的各種研究與應(yīng)用領(lǐng)域，但該模型使用低層抽象信息描述系統(tǒng)中的交互行為，使其逐漸不能滿足復(fù)雜系統(tǒng)的設(shè)計(jì)需求。為此，多種責(zé)任政策的形式化語(yǔ)言和方法被相繼提出，在開發(fā)人工制度[7]、驗(yàn)證程序通信[8]、建模Agent交互[9]等研究領(lǐng)域得到了廣泛的應(yīng)用，這些方法可被分為三類：1) 設(shè)計(jì)政策執(zhí)行語(yǔ)言，如文獻(xiàn)[10]。這類語(yǔ)言可對(duì)政策進(jìn)行簡(jiǎn)單的描述和解釋，但由于缺乏形式語(yǔ)義，所以不能對(duì)其進(jìn)行形式分析或性質(zhì)驗(yàn)證。2) 設(shè)計(jì)政策分析語(yǔ)言，如文獻(xiàn)[11-12]。它們?cè)试S對(duì)政策進(jìn)行形式化定義與分析，但是這類方法沒有定義政策語(yǔ)言執(zhí)行與管理的動(dòng)態(tài)操作語(yǔ)義，不能作為自動(dòng)驗(yàn)證技術(shù)的形式化基礎(chǔ)。3) 文獻(xiàn)[13]直接給出了策略模型的驗(yàn)證方法，但是沒有研究策略模型的形式語(yǔ)義，使策略模型不易被理解和解釋，無法建模更為復(fù)雜的交互策略。針對(duì)上述問題，本文提出一種多Agent交互策略模型檢測(cè)方法，旨在彌補(bǔ)上述兩類方法的不足。該方法中的責(zé)任政策框架語(yǔ)言既可以對(duì)政策進(jìn)行描述和解釋，又允許對(duì)政策進(jìn)行形式化定義與分析，最終支持使用自動(dòng)化工具執(zhí)行驗(yàn)證分析。

1 責(zé)任政策語(yǔ)言

責(zé)任政策描述了多Agent之間的交互策略，即Agent被允許或禁止保持某種狀態(tài)或執(zhí)行某些活動(dòng)，并關(guān)聯(lián)著一些條件集合，這些條件以環(huán)境的形式存在于責(zé)任描述中，描述系統(tǒng)狀態(tài)以及政策的應(yīng)用規(guī)則。因此，在定義責(zé)任政策語(yǔ)言前，先定義責(zé)任政策環(huán)境。與責(zé)任相關(guān)的環(huán)境主要有基于狀態(tài)的環(huán)境和基于事件的環(huán)境?；跔顟B(tài)的環(huán)境聲明政策中責(zé)任的狀態(tài)環(huán)境，基于事件的環(huán)境聲明責(zé)任被激活、失效、違反或履行的時(shí)刻?；跔顟B(tài)的責(zé)任環(huán)境表達(dá)式為：，其形式語(yǔ)義定義為當(dāng)命題公式為真，向承諾時(shí)所在的環(huán)境有效?；谑录沫h(huán)境則描述了基于狀態(tài)的環(huán)境開始有效和終止有效的時(shí)刻，其被聲明為和。責(zé)任政策的環(huán)境表達(dá)式如下：

定義 1 責(zé)任(Obligation)。責(zé)任是一個(gè)六元組，其中，是責(zé)任標(biāo)識(shí)符，是責(zé)任的發(fā)起方，是責(zé)任的接收方，是聲明責(zé)任內(nèi)容的邏輯公式，是責(zé)任的激活環(huán)境，是責(zé)任的違反環(huán)境。責(zé)任被聲明后，將向傳遞由表示的事實(shí)或需要執(zhí)行的動(dòng)作，和分別聲明了責(zé)任被激活和違反的環(huán)境。

定義 2 責(zé)任政策語(yǔ)言(obligation policy language, OPL)。是一個(gè)六元組，其中，是政策中所有Agent的集合，，，既可以是責(zé)任的也可以是；是政策中所有責(zé)任的集合；是政策環(huán)境的集合；是政策動(dòng)作的集合，是責(zé)任操作動(dòng)作的集合，是責(zé)任內(nèi)容中動(dòng)作的集合，即責(zé)任內(nèi)容中承諾執(zhí)行的動(dòng)作；是責(zé)任政策執(zhí)行需滿足的時(shí)序性質(zhì)集合。是一個(gè)責(zé)任分配函數(shù)，給出每個(gè)責(zé)任所歸屬的Agent。

2 責(zé)任政策語(yǔ)言的表達(dá)能力

責(zé)任政策語(yǔ)言通過責(zé)任狀態(tài)模型描述交互策略的動(dòng)態(tài)演化，基于操作語(yǔ)義可將交互策略的OPL模型轉(zhuǎn)換為NuSMV的輸入模型。

2.1 責(zé)任狀態(tài)模型

OPL模型中主要包含連續(xù)型責(zé)任和非連續(xù)型責(zé)任。連續(xù)型責(zé)任聲明系統(tǒng)中有維持事物狀態(tài)需求的責(zé)任，在系統(tǒng)中這種責(zé)任從環(huán)境起始直至環(huán)境結(jié)束都要求其保持激活狀態(tài)，如考慮如下責(zé)任，責(zé)任聲明參加養(yǎng)老保險(xiǎn)的職工向管理機(jī)構(gòu)繳費(fèi)不能低于繳費(fèi)下限。其中，是養(yǎng)老保險(xiǎn)參保人員，是養(yǎng)老保險(xiǎn)管理機(jī)構(gòu)，聲明向執(zhí)行繳費(fèi)行為，激活環(huán)境聲明責(zé)任在為真的情況下有效，違反環(huán)境低于費(fèi)款下限被定義為below_limit_paymentlimit_payment，其聲明參保人員繳納保險(xiǎn)費(fèi)低于政策規(guī)定的繳費(fèi)下限的情況。

非連續(xù)型責(zé)任是被激活后可能發(fā)生失效的責(zé)任，其定義條件可表示為。

責(zé)任的狀態(tài)模型描述責(zé)任政策的動(dòng)態(tài)演化過程，根據(jù)責(zé)任類型的定義，責(zé)任狀態(tài)模型被分為兩種：連續(xù)型責(zé)任狀態(tài)模型和非連續(xù)型責(zé)任狀態(tài)模型，分別如圖1和圖2所示。

責(zé)任狀態(tài)模型中的違反狀態(tài)被定義為持久狀態(tài)，即一旦責(zé)任的違反環(huán)境為真且執(zhí)行違反操作，則責(zé)任處于違反狀態(tài)并在后續(xù)的狀態(tài)演化中保持違反狀態(tài)。

2.2 OPL的操作語(yǔ)義

為了將OPL模型轉(zhuǎn)換為NUSMV的輸入模型，本文將OPL的操作語(yǔ)義定義為具有Kripke結(jié)構(gòu)的狀態(tài)遷移系統(tǒng)。

定義 3 遷移系統(tǒng)(transition system, TS)[14]。遷移系統(tǒng)是一個(gè)六元組：，其中，是系統(tǒng)狀態(tài)的有窮集合，是系統(tǒng)動(dòng)作的有窮集合，表示狀態(tài)遷移關(guān)系集合，是系統(tǒng)初始狀態(tài)的有窮集合，是原子命題的有窮集合，是一個(gè)標(biāo)簽函數(shù)。

遷移系統(tǒng)中，系統(tǒng)狀態(tài)由一組取值為真的原子命題集合表示，標(biāo)簽函數(shù)可以將一個(gè)原子命題集合關(guān)聯(lián)到任意狀態(tài)。對(duì)于一個(gè)給定的邏輯公式，如果包含的原子命題使公式成立，則稱狀態(tài)滿足公式，即|=iff() |=。

3 模型檢測(cè)交互策略模型

模型檢測(cè)(model checking)[14]是一種自動(dòng)驗(yàn)證有窮狀態(tài)并發(fā)系統(tǒng)的形式化技術(shù)。在驗(yàn)證過程中，系統(tǒng)被建模為具有Kripke語(yǔ)義結(jié)構(gòu)的狀態(tài)遷移系統(tǒng)，系統(tǒng)規(guī)范被聲明為模態(tài)/時(shí)序邏輯公式，當(dāng)模型滿足規(guī)范時(shí)驗(yàn)證算法給出肯定答案，否則算法會(huì)將導(dǎo)致錯(cuò)誤結(jié)果的事件序列作為反例返回給用戶，為系統(tǒng)漏洞定位和改進(jìn)提供幫助?；谀Ｐ蜋z測(cè)技術(shù)驗(yàn)證多Agent交互策略，首先要將交互策略模型轉(zhuǎn)換為模型檢測(cè)器的輸入模型，本文選用基于Kripke結(jié)構(gòu)作為輸入的NuSMV作為模型檢測(cè)工具驗(yàn)證交互策略。

3.1 轉(zhuǎn)換交互策略模型到NuSMV模型

NuSMV以模型描述程序和時(shí)態(tài)邏輯規(guī)范文本作為輸入。若規(guī)范成立，則輸出為真，否則顯示一個(gè)軌跡，該軌跡解釋規(guī)范為假的原因。NuSMV輸入模型由一個(gè)或多個(gè)模塊組成，其中一個(gè)模塊必須被聲明為主模塊，每個(gè)模塊都可由三部分組成：變量的聲明、變量賦值以及性質(zhì)聲明。模塊內(nèi)部聲明變量并對(duì)變量賦值，賦值操作通常給出變量的初始值，而變量下一個(gè)值是關(guān)于變量當(dāng)前值的表達(dá)式。NuSMV建模語(yǔ)言的具體語(yǔ)法可參照文獻(xiàn)[14]。

本文基于OPL的操作語(yǔ)義，將其轉(zhuǎn)換為NuSMV 的輸入模型，轉(zhuǎn)換過程中每個(gè)Agent被轉(zhuǎn)換為輸入模型的一個(gè)獨(dú)立模塊，并在主模塊中初始化。各Agent的責(zé)任被建模為對(duì)應(yīng)模塊中的枚舉變量，枚舉值為責(zé)任的各個(gè)狀態(tài)。各Agent的責(zé)任所關(guān)聯(lián)的環(huán)境變量被轉(zhuǎn)換為模塊參數(shù)變量及其內(nèi)部中的枚舉變量和布爾變量，與責(zé)任狀態(tài)相關(guān)的責(zé)任操作則被轉(zhuǎn)換為狀態(tài)演化的推理規(guī)則，這種遷移關(guān)系定義在各模塊的ASSIGN部分，責(zé)任的內(nèi)容動(dòng)作被轉(zhuǎn)換為遷移條件定義在模塊的NEXT語(yǔ)句部分。

3.2 被驗(yàn)證性質(zhì)描述

本文采用計(jì)算樹邏輯CTL聲明系統(tǒng)應(yīng)滿足的關(guān)鍵性質(zhì)，CTL的語(yǔ)法定義如下：

定義 5 令為原子命題，通過Backs-Naur范式定義CTL公式為：

式中，路徑量詞A表示沿著所有路徑(無一例外)；E表示沿著至少(存在)一條路徑(可能)；時(shí)態(tài)算子X、F、G、U分別為下一個(gè)狀態(tài)、未來某個(gè)狀態(tài)、所有未來狀態(tài)和直到。

系統(tǒng)被期望滿足的性質(zhì)主要包括安全性和活性性質(zhì)，系統(tǒng)的安全性被描述為壞事一定不會(huì)發(fā)生，其CTL公式形式為AG，系統(tǒng)的活性被描述為前提成立時(shí)好事會(huì)經(jīng)常發(fā)生，其CTL公式的形式為AG(AF)。

4 實(shí)例研究

4.1 系統(tǒng)建模

本文以《城鎮(zhèn)企業(yè)職工基本養(yǎng)老保險(xiǎn)關(guān)系轉(zhuǎn)移接續(xù)暫行辦法》為例(簡(jiǎn)稱《暫行辦法》)，作為多Agent交互策略，創(chuàng)建該策略的OPL模型?！稌盒修k法》對(duì)指導(dǎo)養(yǎng)老保險(xiǎn)領(lǐng)域多Agent交互行為建模具有重要意義，限于篇幅，本文不對(duì)《暫行辦法》的內(nèi)容一一介紹，僅介紹與驗(yàn)證有關(guān)的重要內(nèi)容，具體如下：

第三條給出了跨省流動(dòng)參保人員達(dá)到基本養(yǎng)老保險(xiǎn)待遇領(lǐng)取條件和未達(dá)到待遇領(lǐng)取年齡前，基本養(yǎng)老保險(xiǎn)關(guān)系和個(gè)人賬戶的具體處理辦法，特別強(qiáng)調(diào)了不得辦理退保手續(xù)。

第四條規(guī)定了如何計(jì)算轉(zhuǎn)移基金，增加了按照實(shí)際繳費(fèi)工資的12%轉(zhuǎn)移統(tǒng)籌基金，更好地平衡地方利益。

第六條規(guī)定了參保人保險(xiǎn)關(guān)系不在戶籍所在地，則累計(jì)繳費(fèi)年限必須滿10年，才可在保險(xiǎn)關(guān)系所在地享受基本養(yǎng)老保險(xiǎn)待遇。

第七條規(guī)定了參保人員轉(zhuǎn)移接續(xù)后，符合待遇領(lǐng)取條件的按照國(guó)發(fā)2005年38號(hào)文的規(guī)定享受基本養(yǎng)老金，確保轉(zhuǎn)移人員的基本養(yǎng)老金計(jì)算辦法與其他參保人員的一致性。

4.2 實(shí)驗(yàn)結(jié)果及分析

根據(jù)OPL模型的操作語(yǔ)義及前文定義的轉(zhuǎn)換關(guān)系，與《暫行辦法》的OPL模型對(duì)應(yīng)的NUSMV部分代碼如圖3所示。

該模型被期望滿足性質(zhì)的CTL公式為：AG((.1=fufilled)->AF(.5=fufilled))，其含義為如果Agent履行參保責(zé)任，則其退休一定可以享受養(yǎng)老保險(xiǎn)待遇。將該性質(zhì)輸入NuSMV執(zhí)行驗(yàn)證，檢測(cè)結(jié)果如圖4所示。

圖中，CTL公式的斷言為False，表示《暫行辦法》的NuSMV模型不滿足該公式，即在《暫行辦法》中存在參保人正常參保，退休后卻不能享受養(yǎng)老保險(xiǎn)待遇的情況，通過模型檢測(cè)器的反例展示功能可獲得驗(yàn)證反例的軌跡，如圖5所示。

分析驗(yàn)證反例可發(fā)現(xiàn)錯(cuò)誤的原因在于《暫行辦法》第六條規(guī)定參保人累計(jì)繳費(fèi)年限必須滿10年才可享受基本養(yǎng)老保險(xiǎn)待遇。如果當(dāng)前年齡在50歲以上的參保人，此前由于種種原因未能積累繳費(fèi)年限，則不能享受保險(xiǎn)待遇。《暫行辦法》第三條又規(guī)定參保人員不能提前退保，因此這類參保人員面臨著退休后既不能享受待遇又不能提前退保的尷尬境遇。

文獻(xiàn)[15]給出了一種基于RAISE建模語(yǔ)言和模型檢測(cè)技術(shù)的領(lǐng)域政策形式化分析方法，該方法首先用RAISE建模語(yǔ)言構(gòu)建領(lǐng)域政策的形式化描述，再將這種形式化描述轉(zhuǎn)換為模型檢測(cè)器SPIN的輸入模型，同時(shí)將被驗(yàn)證性質(zhì)聲明為線性時(shí)序邏輯公式，最后使用SPIN自動(dòng)驗(yàn)證政策模型對(duì)被驗(yàn)證性質(zhì)的可滿足性。文獻(xiàn)[15]同樣以《暫行辦法》為研究實(shí)例，并驗(yàn)證了政策的RAISE模型對(duì)線性時(shí)序邏輯公式聲明性質(zhì)的可滿足性。本文的研究方法與文獻(xiàn)[15]對(duì)比，主要有以下不同：1) RAISE建模語(yǔ)言是一種軟件工程領(lǐng)域通用的形式化語(yǔ)言，而本文設(shè)計(jì)的責(zé)任政策語(yǔ)言O(shè)PL是一種面向領(lǐng)域政策的專用建模語(yǔ)言，OPL相比RAISE建模語(yǔ)言更具備政策建模特質(zhì)，且易于理解和使用。2) 文獻(xiàn)[15]將RAISE政策模型轉(zhuǎn)換為模型檢測(cè)器SPIN的輸入模型。本文將OPL政策轉(zhuǎn)換為模型檢測(cè)器NuSMV的輸入模型，文獻(xiàn)[15]只能驗(yàn)證線性時(shí)序邏輯公式聲明的性質(zhì)，而本文既能夠驗(yàn)證線性時(shí)序邏輯公式聲明的性質(zhì)，又能驗(yàn)證計(jì)算樹邏輯聲明的政策性質(zhì)，所以本文的方法可以驗(yàn)證比文獻(xiàn)[15]的方法更為廣泛的政策性質(zhì)。

5 結(jié)束語(yǔ)

基于模型檢測(cè)技術(shù)，本文提出一種多Agent交互策略形式化驗(yàn)證方法，用于驗(yàn)證多Agent系統(tǒng)中交互行為設(shè)計(jì)的正確性，該方法既使交互策略模型具備易于理解和使用形式語(yǔ)義，又能夠自動(dòng)驗(yàn)證設(shè)計(jì)模型的正確性。實(shí)驗(yàn)結(jié)果表明，該方法可有效地發(fā)現(xiàn)并解釋策略模型中存在的錯(cuò)誤，降低驗(yàn)證過程中的人工參與程度，提高驗(yàn)證效率。

參 考 文 獻(xiàn)

[1] LOIZOS M, DAVID P C, PFEFFER A. Specifying and monitoring economic environments using rights and obligations[J]. Autonomous Agents and Multi-Agent Systems, 2010, 20(2): 158-197.

[2] XU Dian-xiang, SANFORD M, LIU Zhao-liang. Testing access control and obligation policies[C]//International Conference on Computing, Networking and Communications. San Diego, CA , USA: IEEE Computer Society, 2013: 540-544

[3] BALDONI M, BAROGLIO C. Constitutive and regulative specifications of commitment protocols: a decoupled approach[J]. Acm Transactions on Intelligent Systems and Technology, 2013, 4(2): 1-25.

[4] 董孟高, 毛新軍, 常志明, 等. 自適應(yīng)多Agent系統(tǒng)的運(yùn)行機(jī)制和策略描述語(yǔ)言SADL[J]. 軟件學(xué)報(bào), 2011, 22(4): 609-624. DONG Meng-gao, MAO Xin-jun, CHANG Zhi-ming, et al. Running mechanism and strategy description language SADL for self-adaptive MAS[J]. Journal of Software, 2011, 22(4): 609-624.

[5] MINSKY N H, ROZENSHTEIN D. A law-based approach to object-oriented programming[C]//Proceedings on Object- Oriented Programming Systems, Languages and Applications. New York, NY, USA: Applied Intelligence, 1987: 482-493.

[6] MINSKY N H, UNGUREANU V. Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems[J]. ACM Transactions on Software Engineering Methodology, 2000, 9(3): 273-305.

[7] FORNARA N, COLOMBETTI M. Specifying and enforcing norms in artificial institutions: a retrospective review[C]// Proceedings of the 9th International Workshop on Declarative Agent Languages and Technologies. Taipei, Taiwan, China: Springer, 2012: 117-119.

[8] EI-MENSHAWY M, BENTAHAR J. Reducing model checking commitments for agent communication to model checking ARCTL and GCTL[J]. Autonomous Agents and Multi-Agent Systems, 2013, 27(3): 375-418.

[9] YOLUM A P . Constraint satisfaction as a tool for modeling and checking feasibility of multiagent commitments[J]. Applied Intelligence, 2013, 39(3): 489-509.

[10] DOUGHERTY D J, FISLER K, KRISHNAMURTHI S. Obligations and their interaction with programs[C]// Proceedings of 12th European Symposium on Research in Computer Security. Dresden, Germany: Springer, 2007: 375-389.

[11] CRAVEN R, LOBO J, MA J, et al. Expressive policy analysis with enhanced system dynamicity[C]// Proceedings of the 4th International Symposium on Information, Computer, and Communications Security. New York, USA: Association for Computing Machinery, 2009: 239-250.

[12] ELRAKAIBY Y, CUPPENS F, CUPPENS-Boulahia N. Formalization and management of group obligations[C]// IEEE International Symposium on Policies for Distributed Systems and Networks. London, England: Springer, 2009: 158-165.

[13] 吳丹, 危勝軍. 基于模型檢測(cè)的策略沖突檢測(cè)方法[J].電子科技大學(xué)學(xué)報(bào), 2013, 42(5): 745-748.

WU Dan, WEI Sheng-jun. Policy conflict detection method based on model checking[J]. Journal of University of Electronic Science and Technology of China, 2013, 42(5): 745-748.

[14] CHRISTEL B, JOOST-PIETER K. Principles of model checking[M]. [S.l.]: MIT Press, 2008.

[15] ZHANG Tao, HUANG Shao-bi, HUANG Hong-tao. Specification and verification of policy using raise and model checking[C]//International Conference on International Conference on BioMedical Engineering and Informatics. Shanghai, China: [s.n.], 2011.

編 輯 黃 莘

The Method of Model Checking Policy of Multi-Agent Interaction

ZHANG Tao1,2, XIE Hong2, and HUANG Shao-bin1

(1. School of Electrical and Information, Northeast Forestry University Harbin 150030; 2. College of Information and Communication Engineering, Harbin Engineering University Harbin 150001)

A verification method of multi-agent interaction policy is proposed based on model checking. The model of system is specified with obligation policy language and it is converted to the input model of model checker NuSMV based on its operational semantics, the properties of system depending on different types of policy conflicts are represented with temporal logic, and the violations of properties are detected by using NuSMV model checker, which can provide the counterexample and trace it back to the errors ininteraction policy. The result shows that the method can improve the efficiency of verifying interaction policy, and it ensures the correctness of the design of Multi-Agent systems.

formal method; model checking; multi-agent system; NuSMV; policy model

TP399

A

10.3969/j.issn.1001-0548.2016.05.016

2015-01-12；

2016-04-20

國(guó)家科技支撐計(jì)劃(2012BAH08B02)；中央高?；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)基金(HEUCF100603, HEUCF041204)；黑龍江省博士后資助項(xiàng)目(3236310148)

張濤(1981-)，男，博士，主要從事分布式計(jì)算與仿真、形式化方法等方面的研究.