王海洋,段振華,田 聰

1(西安電子科技大學(xué) 計算理論與技術(shù)研究所,陜西 西安 710071)

2(綜合業(yè)務(wù)網(wǎng)理論及關(guān)鍵技術(shù)國家重點實驗室(西安電子科技大學(xué)),陜西 西安 710071)

隨著計算機軟硬件系統(tǒng)的飛速發(fā)展,人工智能(artificial intelligence,簡稱AI)[1]理論與技術(shù)日益成熟,并且在計算機領(lǐng)域內(nèi)得到了前所未有的重視,其應(yīng)用領(lǐng)域在逐漸擴(kuò)大及深入.其中,智能機器人越來越多地出現(xiàn)在人們的日常生活中,例如體育產(chǎn)業(yè)中的足球機器人、日常生活中的家用伺服機器人以及工業(yè)自動焊接機器人等.所以,保障AI產(chǎn)品的安全性和可靠性,是如今人們面臨的刻不容緩的問題.模型檢測(model checking)[2]是一種簡單明了并且實現(xiàn)了自動化的、用于驗證軟硬件系統(tǒng)是否滿足人們期望性質(zhì)的技術(shù).它已經(jīng)廣泛應(yīng)用到各類軟硬件系統(tǒng)的性能檢測中,如運輸控制系統(tǒng)、電子商務(wù)、航空航天領(lǐng)域.近年來,模型檢測方法也已經(jīng)應(yīng)用到AI產(chǎn)品的性能檢測中.模型檢測是一種基于邏輯的、應(yīng)用廣泛的、對有限狀態(tài)系統(tǒng)進(jìn)行自動化程序驗證的技術(shù),最早由著名學(xué)者Clarke與Emerson以及Quielle與Sifakis于20世紀(jì)80年代分別提出.在模型檢測中,系統(tǒng)S編碼為遷移系統(tǒng)MS,要驗證的性質(zhì)規(guī)約P用邏輯公式φP表示,驗證系統(tǒng)S是否滿足規(guī)約P,轉(zhuǎn)化為模型MS是否滿足邏輯公式φP.其中,MS滿足公式φP簡寫為MS|=φP.

驗證AI產(chǎn)品的性能需要將其形式化規(guī)約,而MAS[2]是AI中應(yīng)用廣泛的分布式系統(tǒng),它可以將大而復(fù)雜的系統(tǒng)描述成多個彼此可以互相協(xié)調(diào)通信的小而易管理的系統(tǒng),從而完成各自的或者共同的目標(biāo).MAS在表達(dá)實際系統(tǒng)時,通過各智能體之間的通信、合作、互解、協(xié)調(diào)、調(diào)度、管理及控制來表達(dá)系統(tǒng)的結(jié)構(gòu)、功能及行為特性.采用多智能體系統(tǒng)解決實際應(yīng)用問題.該系統(tǒng)具有很強的魯棒性和可靠性,并具有較高的問題求解效率.MAS已經(jīng)廣泛應(yīng)用于各個領(lǐng)域,如智能機器人、交通控制、分布式預(yù)測、監(jiān)控及診斷、分布式智能決策及虛擬現(xiàn)實.MAS引起了眾多技術(shù)領(lǐng)域的廣泛關(guān)注,因此,設(shè)計、實現(xiàn)及驗證該系統(tǒng)的工具顯得尤為迫切.特別是當(dāng)MAS應(yīng)用于安全驗證相關(guān)領(lǐng)域時,驗證其是否滿足設(shè)計要求就顯得尤其重要了.針對多智能體系統(tǒng)的模型檢測方法的研究,已有學(xué)者取得了突出成果[4,5].

本文根據(jù)文獻(xiàn)[6]中提出的 APTL模型檢測方法實現(xiàn)了多智能體系統(tǒng)模型檢測器 MCMAS_APTL,其用APTL公式表示MAS的性質(zhì)用于檢測MAS的性能.APTL公式不僅可以描述經(jīng)典時序邏輯LTL公式可以描述的性質(zhì),而且可以描述與區(qū)間相關(guān)的順序和循環(huán)性質(zhì)以及開放系統(tǒng)和多智能體系統(tǒng)中的與合作和博弈相關(guān)的性質(zhì),因此,用APTL公式可方便描述多智能體系統(tǒng)的性質(zhì).

狀態(tài)爆炸問題是模型檢測過程面臨的常見問題之一,即隨著變量個數(shù)的增多,系統(tǒng)的狀態(tài)空間呈指數(shù)級增長.在模型檢測過程中,能夠緩解空間爆炸問題的技術(shù)有二值判斷圖(BDD)[7]、抽象技術(shù)、限界模型檢測、化簡和假設(shè)-保證推理.MCMAS_APTL是基于APTL的多智能體系統(tǒng)的符號化模型檢測器.它利用APTL公式表達(dá)多智能體系統(tǒng)的性質(zhì),借助工具 MCMAS[8]中的符號化多智能體系統(tǒng)模塊符號化表示要驗證的系統(tǒng),進(jìn)而驗證模型是否滿足給定的APTL公式.該工具不僅可以驗證多智能體系統(tǒng),還可用于驗證普通的反應(yīng)系統(tǒng).

MAS的模型檢測方法已引起眾多學(xué)者的廣泛關(guān)注并且進(jìn)行了深入研究.文獻(xiàn)[9]中提出了驗證 MAS性質(zhì)的限界模型檢測方法,通過擴(kuò)展CTL*得到包括認(rèn)知模態(tài)的邏輯CTL*K.CTL*K可描述同步解釋系統(tǒng)的性質(zhì),而且可描述時序和認(rèn)知兩個方面的性質(zhì).文獻(xiàn)[10]提出了一個基于AUML狀態(tài)機模型的MAS模型檢測機制.文中利用了比較高效的模型檢測工具M(jìn)CMAS.它不僅可用于檢測MAS的認(rèn)知性質(zhì),而且可以檢測MAS的智能體的行為是否正確或智能體之間的合作關(guān)系,但該文獻(xiàn)不能檢測MAS中智能體之間的博弈性質(zhì).文獻(xiàn)[11]提出了一種自動生成控制器的機制,當(dāng)輸入一種機器人模型和任務(wù)環(huán)境以及一種任務(wù)或者機器人的行為后,該控制器就能保證機器人完成任務(wù).該文獻(xiàn)中的方法是首先創(chuàng)造一種符合規(guī)約LTL公式的控制器,其中,任務(wù)規(guī)約用LTL公式描述,如機器人的搜索、救援、覆蓋面以及障礙躲避等.文獻(xiàn)[12]提出了一種在語法層對智能體策略類型進(jìn)行刻畫的系統(tǒng)模型.它允許不同智能體具備不同的策略類型,研究了基于新模型的ATL模型檢測方法并且開發(fā)了檢測工具.文獻(xiàn)[13]研究了下推多智能體系統(tǒng)的模型檢測方法,引入了下推認(rèn)知博弈結(jié)構(gòu)作為模型,涉及到的時序邏輯為ATEL、ATEL*和AEMC.本文中的MCMAS_APTL工具利用了比較高效的模型檢測工具M(jìn)CMAS中的符號化表示系統(tǒng)部分,性質(zhì)規(guī)約用APTL公式描述,其中,APTL公式簡單易懂,表達(dá)能力強,APTL公式可以方便地描述多智能體系統(tǒng)的性質(zhì),所以該工具可方便地用于多智能體系統(tǒng)的性質(zhì)驗證.

本文第1節(jié)簡單介紹交替投影時序邏輯語法、語義及其他基本概念.第2節(jié)闡述多智能體系統(tǒng)模型檢測器MCMAS_APTL的框架和實現(xiàn)過程.第3節(jié)給出機器人足球賽模型檢測實例.第4節(jié)對本文進(jìn)行總結(jié).

1 基礎(chǔ)概念

1.1 交替投影時序邏輯

語法.APTL的語法定義如下:

令P為原子命題的可數(shù)集合,A為代理的可數(shù)集合.其中,p∈P,A?A,Pi(i=1,…,Pm),P和Q為 APTL 公式,○〈〈A〉〉(next)和prj〈〈A〉〉(projection)為基本的 APTL 時序操作符.

語義.為了定義APTL公式的語義,首先需要介紹并發(fā)博弈結(jié)構(gòu)(concurrent game structure,簡稱 CGS)[6,8].CGS是一個七元組C=〈P,A,S,S0,l,Δ,τ〉,其中,P是原子命題的有窮非空集合;A是代理的有窮集合;S是狀態(tài)的有窮非空集合;S0是初始狀態(tài)的有窮非空集合;l:S→2P為標(biāo)記函數(shù),每個狀態(tài)被原子命題集合的子集標(biāo)記;Δa(s)是代理a∈A在狀態(tài)s的可以做出決策的非空集合;ΔA(s)=Δa1(s)× ...×Δak(s)是代理集合A= {a1,...,ak} ∈ 2A在狀態(tài)s的決策向量的非空集合;相應(yīng)地,ΔA(s)簡單表示為Δ(s),表示A中的代理的決策集合;一個決策da,表示代理a在決策d上的決策,dA表示代理集合A?A在決策d的決策.對于每一個狀態(tài)s∈S和決策d∈Δ(s),τ(s,d)∈S將狀態(tài)s和代理集合A的決策d映射到新的狀態(tài).fA為代理集合A在系統(tǒng)C中的一個策略,該策略使得系統(tǒng)生成多條以初始狀態(tài)s0為起始狀態(tài)的路徑.定義out(s,fA)為以狀態(tài)s為起始狀態(tài)策略fA使得系統(tǒng)執(zhí)行生成的所有的路徑集合.詳細(xì)講解見文獻(xiàn)[6].

根據(jù)CGS的定義,在P上定義了一個狀態(tài)s,為P到B={true,false}的投影,即s:P→B.在一個CGS中,以狀態(tài)s為起始節(jié)點的一條路徑λ(s)滿足APTL公式P,標(biāo)記為λ(s)|=P.一個CGSC滿足APTL公式P當(dāng)且僅當(dāng)所有以CGS的初始節(jié)點為起始節(jié)點的路徑滿足公式P,標(biāo)記為C|=P.

關(guān)系定義如下:

·λ(s)|=p對于命題p∈P,當(dāng)且僅當(dāng)p∈l(s).

·λ(s)|=?P當(dāng)且僅當(dāng)λ(s)|≠P.

·λ(s)|=P∨Q當(dāng)且僅當(dāng)λ(s)|=P或λ(s)|=Q.

·λ(s)|=○〈〈A〉〉P當(dāng)且僅當(dāng)|λ(s)|≥2,并且A存在一個策略fA,使得λ(s)∈out(s,fA),并且λ(s)[1,|λ|]|=P.

·λ(s)|=(P1,…,Pm)prj〈〈A〉〉Q當(dāng)且僅當(dāng)A存在一個策略fA,λ(s)∈out(s,fA),0=r0≤r1≤…≤rm≤|λ(s)|,使得λ(s)[ri-1,ri]|=Pi,0

a)rm<|λ(s)|,那么λ=λ(s)↓(r0,…,rm)·λ(s)[rm+1,…,|λ(s)|];

b)rm=|λ(s)|,那么λ=λ(s)↓(r0,…,rm).

APTL范式.將APTL公式轉(zhuǎn)化為范式(normal form)[6]形式,是APTL模型檢測中不可或缺的環(huán)節(jié).接下來簡單介紹APTL公式的范式和完全范式(complete normal form)的定義.

定義1(范式(normal form)).QP為APTL公式Q中的原子命題集合,公式Q的范式定義為

Qe為狀態(tài)公式,為qk或?qk,如果i≠j,則為 APTL 公式.

APTL公式的范式包含兩部分:Qe∧ε為終止部分,若只有1個狀態(tài)s0的路徑滿足公式Qe,則滿足Qe∧ε;Qci∧Qi為非終止部分,公式Qci∧Qi的模型為一個生成樹,其中,該生成樹的根節(jié)點滿足Qci.

定義2(完全范式(complete normal form)).QP為APTL公式Q中出現(xiàn)的原子命題組成的集合,Q的完全范式定義為,其中,為狀態(tài)公式;為qk或?qk;并且是原子命題的最小項,如果有n個原子命題,就有 2n個最小項m0,m1,…,是原子命題的最大項,也有2n個最大項.

文獻(xiàn)[14]中的定理4已經(jīng)證明,任意一個APTL公式都可以轉(zhuǎn)化為范式.將公式Q轉(zhuǎn)化為范式后,進(jìn)一步可以轉(zhuǎn)化為完全范式.如果Q的完全范式為,則?Q的范式為.

1.2 符號模型檢測

模型檢測是一種有效驗證有限狀態(tài)系統(tǒng)性質(zhì)的技術(shù).由于基于枚舉的模型檢測方法容易造成狀態(tài)爆炸問題,所以在實際應(yīng)用中會遇到很多問題.研究者們嘗試解決該問題,提出了一些緩解模型檢測過程中狀態(tài)爆炸問題的有效方法,如抽象技術(shù)、限界模型檢測以及基于BDD的符號模型檢測.符號模型檢測的核心思想是建立在將狀態(tài)集合和遷移關(guān)系集合用布爾方程表示的基礎(chǔ)上的,用布爾方程隱式地描述狀態(tài)集合和遷移關(guān)系集合,比顯式地利用枚舉方式描述能夠顯著節(jié)約存儲空間.符號化模型檢測方法是以狀態(tài)集合為操作對象,而不是單個狀態(tài).

符號化表示方法能夠更加簡潔地表示系統(tǒng)狀態(tài),本文利用二值判斷圖(binary decision diagrams,簡稱BDD)表示狀態(tài)集合.通過對BDD操作,容易實現(xiàn)求狀態(tài)集合的前驅(qū)狀態(tài)集合、后繼狀態(tài)集合以及狀態(tài)集合的合并等.符號化模型檢測算法與枚舉模型檢測算法的基本搜索過程相似,本質(zhì)區(qū)別在于,一般的模型檢測中以單個狀態(tài)為操作對象;而符號模型檢測中以狀態(tài)集合為操作對象,且借助 BDD等數(shù)據(jù)結(jié)構(gòu),已經(jīng)有功能強大的操作工具包作為后續(xù)開發(fā)基礎(chǔ).

二值判斷圖(BDD).BDD表示布爾函數(shù)的有根無環(huán)有向圖,內(nèi)部節(jié)點標(biāo)記對應(yīng)公式中的變量,葉子節(jié)點標(biāo)記為0或1.如圖1所示為布爾函數(shù)的BDD.

Fig.1 BDD off( a, b, c, d)=a∧b∨c∧圖1f( a, b, c, d)=a∧b∨c∧ 的BDD

一個布爾公式可由不同的BDD表示,為確保每個布爾公式對應(yīng)唯一的BDD,對BDD有兩種限制:(1)對布爾公式中的變量進(jìn)行排序,如圖1中布爾公式變量排序為a

1.3 MCMAS

MCMAS是一種多智能體模型檢測工具,MCMAS的框架結(jié)構(gòu)如圖2所示.

MCMAS具有成熟、高效的符號化技術(shù),我們借助MCMAS中模型的符號化模塊實現(xiàn)APTL模型檢測工具M(jìn)CMAS_APTL.MCMAS利用解釋系統(tǒng)編程語言(interpreted system programming language,簡稱ISPL)描述要驗證的系統(tǒng),支持的邏輯為 CTLKD-ADC[8].將要驗證的系統(tǒng)和一組公式輸入 MCMAS,可計算出系統(tǒng)是否滿足公式.如果公式不成立,則輸出一條反例路徑;否則,輸出一條證據(jù)路徑.

在MCMAS中要驗證的程序形式化表示為解釋系統(tǒng)(interpreted system)并用語言ISPL描述.ISPL程序?qū)⒁环N多智能體系統(tǒng)描述為包含多個智能體和環(huán)境的系統(tǒng),對于 ISPL描述的智能體簡單介紹如下.局部狀態(tài)(local states)是智能體的私有內(nèi)部狀態(tài),是由變量描述的,對于其他智能體是不可見的.智能體與其他智能體和環(huán)境的互動是通過將局部狀態(tài)轉(zhuǎn)化為公共可視化的變量完成的.智能體采取的動作(action)由智能體的局部協(xié)議(local protocol)決定.局部狀態(tài)隨局部演變函數(shù)變化,該類函數(shù)根據(jù)當(dāng)前的局部狀態(tài)和所有智能體的全局動作(joint action)給出可能的下一個局部狀態(tài)(next local state).ISPL程序的結(jié)構(gòu)是根據(jù)IS的語義給出的,并且可以廣泛應(yīng)用于描述多智能體系統(tǒng).在程序中,環(huán)境用關(guān)鍵字Environment表示,Environment中的一些局部變量對其他智能體可見.

Fig.2 Architecture of model checking tool MCMAS圖2 模型檢測工具M(jìn)CMAS的結(jié)構(gòu)框架

2 原型工具

從底層開發(fā)實現(xiàn)模型檢測工具耗時、耗力,不可控因素較多,本文以開源工具為基礎(chǔ)實現(xiàn)我們提出的模型檢測器.鑒于MCMAS工具所具有的特性和優(yōu)點,最終選擇以MCMAS為基礎(chǔ)實現(xiàn)APTL符號模型檢測算法.

2.1 工具框架

我們開發(fā)實現(xiàn)了用于驗證多智能體系統(tǒng)的APTL符號模型檢測器MCMAS_APTL.該工具借助了MCMAS的符號化表示模型.MCMAS_APTL的架構(gòu)如圖3所示.

Fig.3 Architecture of model checking tool MCMAS_APTL圖3 模型檢測工具M(jìn)CMAS_APTL的結(jié)構(gòu)框架

MCMAS_APTL采用 C++語言開發(fā),由 3個模塊組成,分別為:用布爾函數(shù)符號化表示解釋系統(tǒng)模塊;將APTL公式轉(zhuǎn)化為范式模塊;檢查解釋系統(tǒng)是否滿足 APTL公式模塊.第 1個模塊是將解釋系統(tǒng)符號化表示,該模塊是借助工具M(jìn)CMAS中的對應(yīng)的部分;第2個模塊是將APTL公式轉(zhuǎn)化為范式;第3個模塊是通過計算滿足公式的狀態(tài)集合驗證輸入的解釋系統(tǒng)是否滿足給定的APTL公式.

2.2 模型檢測方法

符號模型檢測方法有效緩解狀態(tài)爆炸問題的關(guān)鍵環(huán)節(jié)是用布爾方程符號化表示模型,進(jìn)而用ROBDD高效地表示;后續(xù)整個檢查過程操作都是在ROBDD上進(jìn)行的.APTL符號模型檢測方法是將多智能體系統(tǒng)模型化為解釋系統(tǒng)后進(jìn)行檢測的.解釋系統(tǒng)是Kripke結(jié)構(gòu)的一種擴(kuò)展,與CGS相比更適合MAS的建模.在CGS中系統(tǒng)只有全局狀態(tài)這一概念,IS的全局狀態(tài)是由內(nèi)部所有智能體的局部狀態(tài)組成.詳細(xì)的比較見文獻(xiàn)[6].

2.2.1 符號化表示解釋系統(tǒng)

下面簡單介紹符號化表示解釋系統(tǒng)(interpreted system)的方法.給定一個解釋系統(tǒng).

· 編碼一個智能體i(i∈N)的局部狀態(tài)需要個布爾變量,編碼系統(tǒng)的全局狀態(tài)g為布爾向量,其中,.

· 一個智能體的協(xié)議可用局部狀態(tài)和行為的布爾公式蘊含關(guān)系編碼.是所有協(xié)議的布爾函數(shù)組合得到的整個系統(tǒng)協(xié)議布爾函數(shù).

· 一個智能體的演變函數(shù)是由該智能體的局部變量和其他智能體行為以及環(huán)境的可視化變量組成的布爾函數(shù)表示,t(v,w,v′)為所有智能體演變函數(shù)的布爾函數(shù)組合得到的整個系統(tǒng)演變關(guān)系布爾函數(shù).

解釋系統(tǒng)IS的時序遷移關(guān)系可以用布爾方程Rt(g,g′)表示.該方程由所有代理的演變方程ti得到,即

該公式描述全局狀態(tài)間的布爾關(guān)系,應(yīng)用于時序邏輯操作符的計算.可達(dá)全局狀態(tài)集合G可以用一個布爾公式表示,并通過求解的不動點得到.其中,Q為系統(tǒng)狀態(tài)集合.τ的不動點可通過迭代計算τ(?)得到[1].

2.2.2 APTL符號模型檢測器的實現(xiàn)

定義3(滿足性質(zhì)的狀態(tài)集合).對于一個APTL公式φ和解釋系統(tǒng),其中一條執(zhí)行路徑λ是系統(tǒng)IS中的非空狀態(tài)序列,λ為有窮或者無窮路徑.集合Sat(φ)?G包含了所有的至少有1條以其為初始節(jié)點的路徑滿足公式φ的狀態(tài):

其中,G為系統(tǒng)IS的全局狀態(tài)集合,Paths(G)表示全局狀態(tài)組成的所有的路徑集合.

· 若Satv(?φ)·S0v=0,則表明Sat(?φ)和S0的交集為空,即不存在一條路徑λ∈Paths(g0)(g0∈S0),使得λ|=?φ.即IS中的所有執(zhí)行路徑滿足公式φ;

· 如果Satv(?φ)·S0v≠ 0,則說明在IS中至少存在1條以狀態(tài)集合Sat(?φ)∩S0中的狀態(tài)為起始狀態(tài)的執(zhí)行路徑λce,使得λce|=?φ.

函數(shù)APTL_model_checking(bdd_parameters*para,char*φ)的偽代碼如下所示.

其中,函數(shù)APTL_model_checking中的第1行是計算滿足公式?φ的狀態(tài)集合的BDD,第2行是計算滿足公式?φ的狀態(tài)集合與系統(tǒng)的初始狀態(tài)集合的交集,para→in_st為表示系統(tǒng)的初始狀態(tài)集合的BDD.

函數(shù)BDD cal_aptl_bdd(bdd_parameters*para,char*φ)計算滿足APTL公式φ的狀態(tài)集合的BDD,形參為系統(tǒng)模型的符號化表示參數(shù)和 APTL公式φ,返回的是表示滿足公式φ的狀態(tài)集合的 BDD.其中,“+”和“·”分別代表邏輯“或”和“與”,Satv(φ)為Sat(φ)的布爾方程.NF(φ)是將公式φ轉(zhuǎn)化為范式的過程,是計算Satv(?)的前驅(qū)狀態(tài)函數(shù).計算的不動點.

函數(shù)BDDcal_aptl_bdd(bdd_parameters*para,char*φ)中,第 2 行將公式φ轉(zhuǎn)化為范式,其中,ψi≡φe∧ε或者ψi≡;第4行中,para→vec_reachRT為系統(tǒng)模型的遷移關(guān)系.函數(shù)cal_aptl_bdd首先將APTL公式φ轉(zhuǎn)化為范式,后續(xù)分別處理各項ψi.

· 如果ψi≡φe∧ε,根據(jù)范式的定義,φe為狀態(tài)公式,表示滿足φe的狀態(tài)集合,并且這些狀態(tài)是有窮執(zhí)行路徑的最終狀態(tài).

最后,布爾方程Satv(φ)可以將所有的求“或”得到,即.

3 機器人足球賽模型檢測實例

機器人足球賽[15]是多智能體系統(tǒng)的典型應(yīng)用,其中涉及到了機器人之間的合作與競爭.在足球比賽過程中,同一個組的機器人合作,盡可能地將球踢入對方球門,而對方機器人會盡力阻止足球進(jìn)入自己球隊球門.這個過程要求機器人能夠根據(jù)不同的情景選取不同的策略,其中的合作和博弈性質(zhì)可以方便地用 APTL公式描述.所以,本文通過機器人足球賽的簡單示例展示該工具的工作效果.

3.1 機器人足球賽的策略模型

本節(jié)介紹機器人足球賽的策略模型.

3.1.1 足球場地模型

機器人足球賽場地為長方形,一般是長9 000mm、寬6 000mm.整個球場分為3個區(qū)域:前場、中場、后場,這3個區(qū)域是用直線分隔開的.足球場地模型如圖4所示,場地被量化為長30個單位、寬20個單位,每個單位代表300mm.(x,y)坐標(biāo)表示球場中的位置,中央點的坐標(biāo)為(15,10),中圈的半徑為3個單位長度.球門寬度為4個單位長度,兩個球門線的坐標(biāo)分別為(0,8),(0,12)和(30,8),(30,12).禁區(qū)寬為4個單位長度,長為8個單位長度.

Fig.4 Soccer field model圖4 足球場模型

3.1.2 策略模型

由于機器人足球賽的參數(shù)隨著比賽的進(jìn)行而變化,所以機器人足球賽的路徑規(guī)劃問題比較復(fù)雜.在比賽中,足球機器人不僅要考慮本隊的策略和規(guī)劃,而且要考慮對方球隊機器人可能的策略.所以在一個特定的場景下,可能有多個不同的最優(yōu)選擇.機器人足球賽的規(guī)則和人類足球賽規(guī)則類似.一般地,一個機器人可以采取的行動如下.

· 開球(kick off):在比賽開始時,一個機器人將球踢出.

· 防護(hù)(go to defend):機器人去防護(hù)對方球員.

· 靠近球(go to the ball):機器人靠近球.

· 截球(intercept the ball):當(dāng)對方球員持球時,試圖截取球.

· 傳球(pass the ball to its teammate):當(dāng)持球的機器人被對方球員攔截時,該機器人將球傳給本隊隊員.

· 射門(shoot the ball into the goal):機器人球員試圖將球踢入對方球門.

· 帶球前行(go forward with the ball):機器人持球向距離對方球門近的地方前行.

在比賽過程的任意時刻,每一個機器人都能獲取球的位置、兩個球門的位置、自身的位置和其他機器人的位置.根據(jù)不同的情形,團(tuán)隊中的球員擔(dān)當(dāng)不同的角色,其中包括前鋒(striker)、中場(midfielder)和后衛(wèi)(defender).守門員與其他球員不同.在整場比賽過程中,守門員的角色不變,其程序也比較簡單,僅是一直在尋找、發(fā)現(xiàn)和觀察球的情況.當(dāng)球靠近球門時,守門員試圖將球踢出以防對方球隊進(jìn)球,并且試圖將球踢到距離本隊球門較遠(yuǎn)的位置.對于一場機器人足球賽,持球的球隊采取攻擊策略(attack tactic),對方球隊采取防衛(wèi)策略(defensive tactic).下面詳細(xì)介紹包含兩個球隊A和B的足球賽策略,每隊各有4名球員.

防衛(wèi)策略(defensive tac tic).當(dāng)足球在A隊的中場或者后場時,A隊采取防衛(wèi)策略.如果A隊沒有隊員持球,那么A隊中距離球最近的隊員試圖截球,該球員作為后衛(wèi).距離對方球門最近的隊員跑去中場并作為前衛(wèi),當(dāng)本隊球員截取到球后等待著傳球.另外一個球員作為中場隊員,并且試圖去攔截對方球員的傳球.該場景如圖5(a)所示,紅色隊員屬于A隊,黃色隊員屬于B隊.其中GK為守門員、S為前鋒、M為中場、D為后衛(wèi).如果A隊隊員持球,持球的機器人作為中場隊員且必須將球傳給前鋒.剩余的一個隊員作為后衛(wèi)并且停留在罰球點(penalty spot).當(dāng)前鋒得到球后采取新的策略,該隊員將會有新的角色或者行為.該情形如圖5(b)所示.

Fig.5 Role assignment in a defensive tactic圖5 防衛(wèi)策略中的角色分配

進(jìn)攻策略(offensive tactic).當(dāng)球在前場時,A隊采取進(jìn)攻策略.如果A隊隊員持球,持球隊員作為前鋒,距離本隊球門最近的隊員作為后衛(wèi)且站在罰球點以防對方球員進(jìn)球.另一個隊員作為中場隊員與前鋒保持在一個水平線上并且在離對方球門近的地方,如果對方球員沒有在球門和前鋒之間攔截球,那么前鋒將球踢向?qū)Ψ角蜷T.如果對方球員試圖攔截球,那么前鋒將球傳給中場隊員,并選擇新的策略.以上兩種情形如圖6所示.如果A隊沒有隊員持球,A隊中的前鋒試圖截球.后衛(wèi)必須在后場以防對方球員進(jìn)球.中場球員阻擋對方隊員靠近自己區(qū)域以防對方隊員之間傳球.

Fig.6 Role assignment in a offensive tactic圖6 進(jìn)攻策略中的角色分配

3.2 實驗展示

首先,我們根據(jù)上述介紹的足球賽策略用 ISPL描述機器人足球賽過程;然后,用工具 MCMAS_APTL展示比賽過程并驗證是否兩個球隊都有可能進(jìn)球.球隊分為紅、黃兩個隊,每隊有3名隊員.足球場地模型如圖4所示,守門員的活動區(qū)域為罰球區(qū).

守門員可以采取的動作包括act_none、run、intercept和kick the ball.顯然,act_none表示守門員不行動;run表示守門員前進(jìn);intercept表示守門員攔截對方球員進(jìn)球;kick the ball表示守門員踢球.前鋒和中場可以采取的動作包括 act_none、kick off、kick the ball、run、intercept、shoot、pass the ball、take a pass和 dribbling.kick off表示球員在比賽開始時開球;pass the ball表示球員將球傳遞給本隊球員;shoot表示球員試圖將球踢入對方球門;take a pass表示球員得到本隊球員傳的球;dribbling表示球員持球前行.

足球賽的模型描述為一個解釋系統(tǒng),紅隊包含3個代理(agent):r_gk、r_1和r_2,其中,r_gk為守門員;r_1和r_2根據(jù)實際情況有3個角色——前鋒(striker)、中場(midfielder)和后衛(wèi)(defender).黃隊也有3個代理:y_gk,y_1和y_2,角色分配與紅隊類似.代理environment包含可視變量用于描述比賽過程中的環(huán)境.

以r_1為例介紹機器人的部分行為,kick off表示代理r_1在比賽開始時開球,代碼如下所示.

其中,(Environment.ballx,Environment.bally)表示球的位置坐標(biāo),(Environment.red_gkx,Environment.red_gky)表示代理red_gk的位置坐標(biāo),其他類似.Vars中的state為代理r_1的狀態(tài)變量,括號內(nèi)為r_1的所有可能的狀態(tài)取值.Actions為r_1的所有的行為動作.Protocol為r_1的協(xié)議,如,state=kick_off:{kickoff}表示當(dāng)r_1的狀態(tài)為kick_off時,其采取的行動為kickoff.Evolution是代理r_1的演變函數(shù),例如代碼中r_1的演變函數(shù),當(dāng)if后面的公式的值為真時,代理r_1的狀態(tài)為kick_off;如果代理在某一狀態(tài)時同時有多個if后面的公式的值為真,則代理的狀態(tài)是在幾個可能的狀態(tài)中隨機選取的.

行為passtheball表示代理r_1傳球給隊友r_2.如果r_1持球并且無法將球踢入對方球門,那么r_1采取passtheball行動,同時,對方球隊隊員會試圖截球,passtheball的代碼如下所示.

當(dāng)y_1或者y_2持球并且條件對r_1有利,r_1可能采取intercept行為,該情況下ISPL代碼如下所示:

對于該系統(tǒng),原子命題集合AP={redscore,yellowscore},redscore表示紅隊進(jìn)球得分,yellowscore表示黃隊進(jìn)球得分;代理分為兩個組g1={r_gk,r_1,r_2}和g2={y_gk,y_1,y_2}.為了得到黃隊進(jìn)球得分的路徑,我們給出APTL公式,如果黃隊能夠進(jìn)球,會輸出一條路徑滿足.其中,公式的語義為代理集合g2存在策略使得執(zhí)行路徑上存在狀態(tài)滿足原子命題公式y(tǒng)ellowscore.如圖7所示為一條滿足公式的路徑,其中,足球從中央點(15,10)經(jīng)由曲線到達(dá)點(0,11),球到點(0,11)表明黃隊已進(jìn)球,該曲線為比賽過程中足球的運動軌跡.

另外,本文實現(xiàn)了一場每隊有兩名隊員的機器人足球賽,球隊的策略與第 3.1節(jié)介紹的策略類似.原子命題集合為表示紅隊得分進(jìn)球,yellowscore表示黃隊得分進(jìn)球.系統(tǒng)包含兩支球隊分別為.

在球賽開始時,代理red_f開球.如果想要得到紅隊進(jìn)球得分的一條路徑,給出APTL公式,當(dāng)紅隊進(jìn)球得分時,MCMAS_APTL輸出一條路徑滿足公式,如圖8所示.

Fig.7 A path satisfies 圖7 滿足的路徑

Fig.8 A path satisfies 圖8 滿足的路徑

另外,本文實現(xiàn)了每個球隊包含兩個隊員的實驗,其中,模擬過程執(zhí)行時間、可達(dá)狀態(tài)數(shù)以及所用的BDD存儲空間如表1中2×2這一行所示.與每個球隊有兩個球員的比賽相比,每個球隊有3個球員的比賽所用時間明顯增多,狀態(tài)空間爆發(fā)式增長.這兩種實驗都是在2.93GHZ Intel Core i7,8GB RAM上完成的.實驗結(jié)果表明,工具 MCMAS_APTL具有一定的實用性,但是要高效地驗證復(fù)雜的多智能體系統(tǒng),還需提高工具 MCMAS_APTL的性能.

Table 1 Performance of MCMAS_APTL for robotic soccer games表1 機器人足球賽在MCMAS_APTL上的執(zhí)行

4 結(jié) 論

本文根據(jù)APTL符號模型檢測算法實現(xiàn)了模型檢測器MCMAS_APTL,將APTL模型檢測算法實現(xiàn)并且融合到 MCMAS中,實現(xiàn)了一種基于 APTL的多智能體系統(tǒng)模型檢測器.在實現(xiàn) MCMAS_APTL時,借助了MCMAS的符號化系統(tǒng)模塊,該部分可高效地符號化表示要驗證的系統(tǒng),從而提高了模型檢測的效率.在工具M(jìn)CMAS_APTL中實現(xiàn)了利用 APTL公式驗證多智能體系統(tǒng)的時序性質(zhì).在未來的工作中,將會研究系統(tǒng)的認(rèn)知性質(zhì)并且實現(xiàn)對多智能體系統(tǒng)認(rèn)知性質(zhì)的檢測.