王海洋,段振華,田 聰

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

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

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

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

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

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

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

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

1 基礎(chǔ)概念

1.1 交替投影時(shí)序邏輯

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

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

語義.為了定義APTL公式的語義,首先需要介紹并發(fā)博弈結(jié)構(gòu)(concurrent game structure,簡稱 CGS)[6,8].CGS是一個(gè)七元組C=〈P,A,S,S0,l,Δ,τ〉,其中,P是原子命題的有窮非空集合;A是代理的有窮集合;S是狀態(tài)的有窮非空集合;S0是初始狀態(tài)的有窮非空集合;l:S→2P為標(biāo)記函數(shù),每個(gè)狀態(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中的代理的決策集合;一個(gè)決策da,表示代理a在決策d上的決策,dA表示代理集合A?A在決策d的決策.對(duì)于每一個(gè)狀態(tài)s∈S和決策d∈Δ(s),τ(s,d)∈S將狀態(tài)s和代理集合A的決策d映射到新的狀態(tài).fA為代理集合A在系統(tǒng)C中的一個(gè)策略,該策略使得系統(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上定義了一個(gè)狀態(tài)s,為P到B={true,false}的投影,即s:P→B.在一個(gè)CGS中,以狀態(tài)s為起始節(jié)點(diǎn)的一條路徑λ(s)滿足APTL公式P,標(biāo)記為λ(s)|=P.一個(gè)CGSC滿足APTL公式P當(dāng)且僅當(dāng)所有以CGS的初始節(jié)點(diǎn)為起始節(jié)點(diǎn)的路徑滿足公式P,標(biāo)記為C|=P.

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

·λ(s)|=p對(duì)于命題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存在一個(gè)策略fA,使得λ(s)∈out(s,fA),并且λ(s)[1,|λ|]|=P.

·λ(s)|=(P1,…,Pm)prj〈〈A〉〉Q當(dāng)且僅當(dāng)A存在一個(gè)策略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模型檢測(cè)中不可或缺的環(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個(gè)狀態(tài)s0的路徑滿足公式Qe,則滿足Qe∧ε;Qci∧Qi為非終止部分,公式Qci∧Qi的模型為一個(gè)生成樹,其中,該生成樹的根節(jié)點(diǎn)滿足Qci.

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

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

1.2 符號(hào)模型檢測(cè)

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

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

二值判斷圖(BDD).BDD表示布爾函數(shù)的有根無環(huán)有向圖,內(nèi)部節(jié)點(diǎn)標(biāo)記對(duì)應(yīng)公式中的變量,葉子節(jié)點(diǎn)標(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

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

1.3 MCMAS

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

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

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

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

2 原型工具

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

2.1 工具框架

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

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

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

2.2 模型檢測(cè)方法

符號(hào)模型檢測(cè)方法有效緩解狀態(tài)爆炸問題的關(guān)鍵環(huán)節(jié)是用布爾方程符號(hào)化表示模型,進(jìn)而用ROBDD高效地表示;后續(xù)整個(gè)檢查過程操作都是在ROBDD上進(jìn)行的.APTL符號(hào)模型檢測(cè)方法是將多智能體系統(tǒng)模型化為解釋系統(tǒng)后進(jìn)行檢測(cè)的.解釋系統(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 符號(hào)化表示解釋系統(tǒng)

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

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

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

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

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

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

2.2.2 APTL符號(hào)模型檢測(cè)器的實(shí)現(xiàn)

定義3(滿足性質(zhì)的狀態(tài)集合).對(duì)于一個(gè)APTL公式φ和解釋系統(tǒng),其中一條執(zhí)行路徑λ是系統(tǒng)IS中的非空狀態(tài)序列,λ為有窮或者無窮路徑.集合Sat(φ)?G包含了所有的至少有1條以其為初始節(jié)點(diǎn)的路徑滿足公式φ的狀態(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行是計(jì)算滿足公式?φ的狀態(tài)集合的BDD,第2行是計(jì)算滿足公式?φ的狀態(tài)集合與系統(tǒng)的初始狀態(tài)集合的交集,para→in_st為表示系統(tǒng)的初始狀態(tài)集合的BDD.

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

函數(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ù)分別處理各項(xiàng)ψi.

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

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

3 機(jī)器人足球賽模型檢測(cè)實(shí)例

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

3.1 機(jī)器人足球賽的策略模型

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

3.1.1 足球場(chǎng)地模型

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

Fig.4 Soccer field model圖4 足球場(chǎng)模型

3.1.2 策略模型

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

· 開球(kick off):在比賽開始時(shí),一個(gè)機(jī)器人將球踢出.

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

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

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

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

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

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

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

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

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

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

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

3.2 實(shí)驗(yàn)展示

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4 結(jié) 論

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