多智能體協(xié)同的認(rèn)知規(guī)范模型檢測(cè)算法*

陳清亮, 朱可宜

(暨南大學(xué)計(jì)算機(jī)科學(xué)系，廣東 廣州 510632)

時(shí)態(tài)邏輯(Temporal Logics)在描述和驗(yàn)證硬件和軟件系統(tǒng)中取得了巨大的成功，是目前形式化驗(yàn)證技術(shù)中的主要工具之一。雖然傳統(tǒng)的時(shí)態(tài)邏輯有著非常廣泛的應(yīng)用，但是對(duì)于描述多智能體系統(tǒng)來(lái)說(shuō)，就顯得有點(diǎn)力不從心了，因?yàn)槎嘀悄荏w系統(tǒng)的狀態(tài)遷移關(guān)系不光和單個(gè)agent有關(guān)，還和agent間的交互，協(xié)同合作有關(guān)，這些都是傳統(tǒng)的時(shí)態(tài)邏輯所沒(méi)法描述的。為此Alur等[1]提出了一種交替時(shí)態(tài)邏輯ATL(Alternating Temporal Logic)來(lái)彌補(bǔ)這個(gè)缺陷，ATL實(shí)際上就是把CTL中的路徑算子換成了協(xié)同算子(cooperation modalities)，用<<Γ>>來(lái)表示，其中Γ就是一組agent。ATL公式<<Γ>>α就表示，Γ中的agent能夠協(xié)同合作使得目標(biāo)α成立，或者說(shuō)，Γ中的agent存在一個(gè)合作策略使得目標(biāo)α成立。而相應(yīng)的ATL的驗(yàn)證工具M(jìn)OCHA也已經(jīng)開發(fā)成熟[2]，因此ATL成了目前研究多智能體協(xié)同合作的一個(gè)最主要的邏輯工具之一[3]。

鑒于認(rèn)知邏輯目前在智能體領(lǐng)域研究的重要性，為了增加ATL的表達(dá)能力，多智能體領(lǐng)域的創(chuàng)始人Wooldridge 等[4]在ATL中加入了認(rèn)知算子(Knowledge modalities)，形成了ATEL (Alternating Temporal Epistemic Logic)，ATEL有著更豐富的表達(dá)能力，能夠表達(dá)諸如CΓα→<<Γ>>β, 即如果智能體組Γ中擁有公共知識(shí)α，那么智能體組Γ能夠合作使得β成立。但是Wooldridge等[4]并沒(méi)有完全給出這些認(rèn)知規(guī)范的模型檢測(cè)算法。

本文將研究ATEL中所有的認(rèn)知算子的檢測(cè)算法問(wèn)題，包括單層的如“智能體a知道什么”，多層的如“智能體a知道智能體b知道什么”，還有分布式知識(shí)，公共知識(shí)等等。將會(huì)看到，認(rèn)知算子的引入并沒(méi)有增加ATL的計(jì)算復(fù)雜性，因此ATEL是一種有效的邏輯工具，在增加表達(dá)力的同時(shí)維持了其計(jì)算的可行性。

1 交替時(shí)態(tài)認(rèn)知邏輯ATEL

1.1 交替認(rèn)知遷移系統(tǒng)

首先我們給出ATEL的語(yǔ)義結(jié)構(gòu)：交替認(rèn)知遷移系統(tǒng)(Alternating Epistemic Transition System)，這個(gè)結(jié)構(gòu)是在定義ATL的語(yǔ)義交替遷移系統(tǒng)(Alternating Transition System)中擴(kuò)展得到的。一個(gè)交替認(rèn)知遷移系統(tǒng)是一個(gè)多元組<Π,Σ,Q,～1,...,～n,π,δ> ,其中，Π是一個(gè)非空有限的命題集合。Σ={a1,...，an} 是一個(gè)有限非空的agent集合。Q是一個(gè)有限非空的狀態(tài)集合。 ～a?Q×Q是表示agenta的認(rèn)知可達(dá)關(guān)系(epistemic accessibility relations)，而根據(jù)標(biāo)準(zhǔn)的認(rèn)知邏輯定義，這個(gè)關(guān)系會(huì)是一個(gè)等價(jià)關(guān)系，即滿足S5公理的標(biāo)準(zhǔn)認(rèn)知邏輯[5]。π:Q→2Π是一個(gè)賦值函數(shù)，把每個(gè)狀態(tài)賦值為在此狀態(tài)下成立的那些命題。δ:Q×Σ→22Q是一個(gè)系統(tǒng)遷移函數(shù)，把每個(gè)狀態(tài)和agent映射到其對(duì)應(yīng)的下一個(gè)可能的狀態(tài)集合，也可以解釋為agent的所有可能的選擇策略。

1.2 認(rèn)知關(guān)系

如果Γ?Σ，用Γ的可達(dá)關(guān)系并集定義為 ～ΓE= (∪a∈Γ～a) 。另外用 ～ΓC來(lái)表示～ΓE的傳遞閉包，下面將用～ΓC和～ΓE來(lái)定義 “公共知識(shí)”和“每個(gè)人都知道”這樣的認(rèn)知模態(tài)詞。

對(duì)于兩個(gè)狀態(tài)q,q′Q以及一個(gè)agentaΣ， 如果有一個(gè)狀態(tài)集合Q′δ(q,a) 使得q′Q′ 那么我們定義q′是狀態(tài)q的 一個(gè)a后繼狀態(tài)(a-succesor)。也就是說(shuō)，q′是a處在狀態(tài)q時(shí)的可能的選擇狀態(tài)集合中的一個(gè)元素。 我們可以用succ(q,a)表示q狀態(tài)下所有的a后繼狀態(tài)集合。如果對(duì)于所有a∈Σ， 都有q′succ(q,a)，我們稱q′是q的后繼，也就是說(shuō)，當(dāng)系統(tǒng)在狀態(tài)q時(shí)，智能體組Σ能協(xié)同合作使得系統(tǒng)進(jìn)入q′狀態(tài)。

一個(gè)AETS的計(jì)算就是一個(gè)無(wú)窮的狀態(tài)序列λ=q0,q1,...使得對(duì)于所有的u>0, 狀態(tài)qu是qu-1的一個(gè)后繼狀態(tài)。 一個(gè)從狀態(tài)q開始的λ計(jì)算就稱為q-計(jì)算；我們也用λ[i]表示計(jì)算中的第i個(gè)狀態(tài)，同樣的，我們也可以用λ[0,i]和λ[i,∞]表示狀態(tài)序列q0,..,qi以及無(wú)窮后綴qi,qi+1,...

1.3 系統(tǒng)的策略和輸出

直覺(jué)來(lái)說(shuō)，一個(gè)策略(strategy)就是一個(gè)智能體的決策過(guò)程的抽象模型。根據(jù)一個(gè)策略，智能體會(huì)從一個(gè)狀態(tài)遷移到另一個(gè)狀態(tài)。嚴(yán)格的定義的話，一個(gè)智能體a的一個(gè)策略是一個(gè)全函數(shù)fa:Q+→2Q, 并且滿足約束：對(duì)于所有的λQ*和qQ,fa(λ·q)δ(q,a). 對(duì)于給定一組智能體Γ和其相應(yīng)的策略FΓ={fa|aΓ}， 定義out(q,FΓ)為系統(tǒng)在狀態(tài)q下，每個(gè)agent都按照自己的策略選擇時(shí)，系統(tǒng)最終的可能的輸出狀態(tài)集合。也就是說(shuō)，out(q,FΓ)包含了Γ中所有的agent按自己的策略協(xié)同合作所產(chǎn)生的所有可能的q-計(jì)算。

1.4 交替時(shí)態(tài)認(rèn)知邏輯ATEL

定義1.1 給定一個(gè)交替認(rèn)知遷移系統(tǒng)S=<Π,Σ,Q,～1,...,～n,π,δ>，在其上定義的一個(gè)ATEL公式，是由以下遞歸規(guī)則所產(chǎn)生的邏輯語(yǔ)言。①原子命題p, 其中pΠ；②φ或φ∨φ，其中φ,φ都是ATEL 公式；③<<Γ>>φ,<<Γ>>φ, 或 <<Γ>>φAφ, 其中Γ是一組agents，φ和φ是一個(gè)ATEL公式；④Kaφ， 其中a是一個(gè)agent，φ是一個(gè)ATEL公式，⑤CΓφ,EΓφ或者DΓφ， 其中Γ是一組agents，φ是一個(gè)ATEL公式。

定義1.2 設(shè)S是上述的一個(gè)交替認(rèn)知遷移系統(tǒng)，q是S中的一個(gè)狀態(tài)，φ是一個(gè)S上的ATEL公式，用S,q|=φ表示φ在q中成立，其余的公式語(yǔ)義按照以下遞歸規(guī)則定義：①S,q|=p當(dāng)且僅當(dāng)pπ(q),pΠ；②S,q|=φ當(dāng)且僅當(dāng)S,q|≠φ；③S,q|=φ∨φ當(dāng)且僅當(dāng)S,q|=φ或者S,q|=φ;④S,q|=<<Γ>>φ當(dāng)且僅當(dāng)存在一個(gè)策略集合FΓ，對(duì)應(yīng)于每個(gè)aΓ, 使得對(duì)于所有的λout(q,FΓ)，有S,λ[1]|=φ；⑤S,q|=<<Γ>>φ當(dāng)且僅當(dāng)存在一個(gè)策略集合FΓ，對(duì)應(yīng)于每個(gè)aΓ, 使得對(duì)于所有的λout(q,FΓ)，有S,λ[u]|=φ對(duì)所有的uN成立；⑥S,q|=<<Γ>>φAφ當(dāng)且僅當(dāng)存在一個(gè)策略集合FΓ，對(duì)應(yīng)于每個(gè)aΓ, 使得對(duì)于所有的λout(q,FΓ)，存在某個(gè)uN使得S,λ[u]|=φ而且對(duì)于所有0≤v

2 ATEL的模型檢測(cè)算法

由于認(rèn)知算子是通過(guò)認(rèn)知可達(dá)關(guān)系(epistemic accessibility relations)定義的, Wooldridge等[5]采用標(biāo)準(zhǔn)的解釋系統(tǒng)(interpreted systems)模型來(lái)等價(jià)轉(zhuǎn)化這些認(rèn)知算子。給定一個(gè)狀態(tài)qQ和一個(gè)agentaΣ，用statea(q)表示agent a 在狀態(tài)q時(shí)局部狀態(tài)(local states)，我們就可以定義認(rèn)知可達(dá)關(guān)系為q～aq′當(dāng)且僅當(dāng) statea(q)=statea(q′)。這樣要檢測(cè)S,q|=Kaφ當(dāng)且僅當(dāng)對(duì)滿足statea(q)=statea(q′)的所有q′，有S,q′|=φ。為此要把一個(gè)抽象的statea(q)用一個(gè)具體的布爾常量s來(lái)表示，即用形式化驗(yàn)證中的符號(hào)化方法編碼一個(gè)狀態(tài)。由[4],有

S,q|=Kaφ

iffS,q|=<<>>((statea=s)→φ) (II)

這樣的公式在ATL中表示為一個(gè)不變式的規(guī)范公式(invariant formula)，進(jìn)而可以用MOCHA軟件進(jìn)行檢測(cè)了[2]。

定理1S,q|=KaKbφiffS,q|=<<>>((statea=sa)→

(<<>>((stateb=sb)→φ)).

證明由(II),S,q|=KaKbφiffS,q|=<<>>((statea=s)→Kbφ) iff

S,q|=<<>>((statea=sa)→

(<<>>((stateb=sb)→φ)).

對(duì)于兩層以上的認(rèn)知規(guī)范，只需要反復(fù)應(yīng)用(II)式即可。

定理2S,q|=EΓφiffS,q|=∩iΓ<<>>((statei=si)→φ) .

證明根據(jù)模態(tài)詞EΓ的定義，EΓφ= ∩iΓKiφ，然后再應(yīng)用(II)式即可。

定理3S,q|=DΓφiffS,q|=<<>>((∩iΓ(statei=si))→φ)

證明根據(jù)分布式認(rèn)知算子的語(yǔ)義[5]，DΓφ表示Γ中所有智能體擁有的信息的交能夠推出φ，結(jié)合(II)式，可以得到結(jié)論。

對(duì)于最復(fù)雜的公共知識(shí)算子CΓ，我們先假設(shè)一個(gè)最簡(jiǎn)單的情形即Γ={a,b}，也就是只有兩個(gè)智能體的情況，然后再把這種證明方法推廣到任意n個(gè)智能體的情形中去。

定理4S,q|=CΓφiff (statea=sa)?(stateb=sb)且S,q|=<<>>((statea=sa)→φ)成立。

證明根據(jù)公共知識(shí)的定義[5]，CΓφ當(dāng)且僅當(dāng)對(duì)所有的有限序列{i1,...,in}{a,b}*，有S,q|=Ki1...Kinφ，這里直接根據(jù)認(rèn)知算子可達(dá)關(guān)系的語(yǔ)義，KaKbφ語(yǔ)義上表示(sa→sb)∧(sb→φ), 而同理，KbKaφ可以等價(jià)于(sb→sa)∧(sa→φ)。再進(jìn)一步，KbKaKbφ可以等價(jià)于(sb→sa)∧(sa→sb)∧(sa→φ)，KaKbKaφ可以等價(jià)于(sa→sb)∧(sb→sa)∧(sb→φ)， 照此類推，可以得到(statea=sa)?(stateb=sb) 且S,q|=<<>>((statea=sa)→φ)成立。

那么對(duì)于任意n個(gè)agent組成的Γ，可以把上述結(jié)論類推就行了。

3 結(jié) 論

本文研究了ATEL中所有的認(rèn)知算子的檢測(cè)算法問(wèn)題, 未來(lái)工作可以在以下幾個(gè)方面，比如ATL中加入另外的非經(jīng)典規(guī)范邏輯如BDI的檢測(cè)問(wèn)題[6]，另外還有相關(guān)的復(fù)雜性討論，完備公理的建立問(wèn)題等[7]。

參考文獻(xiàn)：

[1] ALUR R, HENZINGER T A, KUPFERMAN O. Alternating-time temporal logic[J]. J ACM,2002, 49(5): 672-713.

[2] ALUR R, HENZINGER T A, HENZINGER T A,et al. MOCHA: Modularity in Model Checking. CAV, 1998: 521-525.

[3] WOOLDRIDGE M,?GOTNES T, DUNNE P E,et al. Logic for automated mechanism design - A Progress Report[R]//AAAI 2007: 9-15.

[4] Van der HOEK W, WOOLDRIDGE M.Cooperation, knowledge and time:alternating-time temporal epistemic logic and its applications[J]. Studia Logica,2003,75(1): 125-157.

[5] HALPERN J Y, FAGIN R, MOSES Y, et al. Reasoning About Knowledge[M]. MIT Press, 1995.

[6] SU K, SATTAR A, WANG K, et al. Observation-based Model for BDI-Agents[C]. AAAI 2005: 190-195.

[7] Van der HOEK W, LOMUSCIO A, WOOLDRIDGE M. On the complexity of practical ATL model checking[C]//AAMAS 2006: 201-208.