張 濤，謝 紅，黃少濱

?

多Agent交互策略模型檢測方法

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

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

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

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

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

1 責(zé)任政策語言

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

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

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

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

責(zé)任政策語言通過責(zé)任狀態(tài)模型描述交互策略的動態(tài)演化，基于操作語義可將交互策略的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)老保險的職工向管理機構(gòu)繳費不能低于繳費下限。其中，是養(yǎng)老保險參保人員，是養(yǎng)老保險管理機構(gòu)，聲明向執(zhí)行繳費行為，激活環(huán)境聲明責(zé)任在為真的情況下有效，違反環(huán)境低于費款下限被定義為below_limit_paymentlimit_payment，其聲明參保人員繳納保險費低于政策規(guī)定的繳費下限的情況。

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

責(zé)任的狀態(tài)模型描述責(zé)任政策的動態(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的操作語義

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

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

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

3 模型檢測交互策略模型

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

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

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

本文基于OPL的操作語義，將其轉(zhuǎn)換為NuSMV 的輸入模型，轉(zhuǎn)換過程中每個Agent被轉(zhuǎn)換為輸入模型的一個獨立模塊，并在主模塊中初始化。各Agent的責(zé)任被建模為對應(yīng)模塊中的枚舉變量，枚舉值為責(zé)任的各個狀態(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)容動作被轉(zhuǎn)換為遷移條件定義在模塊的NEXT語句部分。

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

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

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

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

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

4 實例研究

4.1 系統(tǒng)建模

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

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

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

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

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

4.2 實驗結(jié)果及分析

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

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

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

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

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

5 結(jié)束語

基于模型檢測技術(shù)，本文提出一種多Agent交互策略形式化驗證方法，用于驗證多Agent系統(tǒng)中交互行為設(shè)計的正確性，該方法既使交互策略模型具備易于理解和使用形式語義，又能夠自動驗證設(shè)計模型的正確性。實驗結(jié)果表明，該方法可有效地發(fā)現(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)的運行機制和策略描述語言SADL[J]. 軟件學(xué)報, 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] 吳丹, 危勝軍. 基于模型檢測的策略沖突檢測方法[J].電子科技大學(xué)學(xué)報, 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

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

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