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

張 濤，謝 紅，黃少濱

?

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

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

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

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

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

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

1 責任政策語言

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

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

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

2 責任政策語言的表達能力

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

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

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

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

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

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

2.2 OPL的操作語義

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

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

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

3 模型檢測交互策略模型

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

3.1 轉換交互策略模型到NuSMV模型

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

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

3.2 被驗證性質描述

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

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

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

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

4 實例研究

4.1 系統(tǒng)建模

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

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

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

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

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

4.2 實驗結果及分析

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

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

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

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

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

5 結束語

基于模型檢測技術，本文提出一種多Agent交互策略形式化驗證方法，用于驗證多Agent系統(tǒng)中交互行為設計的正確性，該方法既使交互策略模型具備易于理解和使用形式語義，又能夠自動驗證設計模型的正確性。實驗結果表明，該方法可有效地發(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] 董孟高, 毛新軍, 常志明, 等. 自適應多Agent系統(tǒng)的運行機制和策略描述語言SADL[J]. 軟件學報, 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].電子科技大學學報, 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è)務費專項基金(HEUCF100603, HEUCF041204)；黑龍江省博士后資助項目(3236310148)

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