施曉靜，張晉津

(1.南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,江蘇 南京 210016；2.南京審計(jì)學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)系,江蘇 南京 211815)

0 引 言

由于分布式計(jì)算技術(shù)的進(jìn)步，將分布式技術(shù)與人工智能相結(jié)合，從而得到的分布式人工智能正逐漸受到研究專家和學(xué)者的重視。分布式人工智能的研究主要集中在多agent之間的合作、交互等方面[1]。因此，在大多數(shù)情況下，一個(gè)agent就需要同其他agent聯(lián)合起來(lái)去解決一個(gè)問(wèn)題，在這種情形下，各個(gè)agent間進(jìn)行信息傳遞與信息更新是不可避免的。如何形式化地刻畫agent的認(rèn)知所遵循的邏輯規(guī)律成為學(xué)者們最關(guān)心的問(wèn)題之一。

Hans vanDitmarsch等引入了未來(lái)事件邏輯(future event logic,FEL)[1]，通過(guò)在模態(tài)邏輯中添加新算子?φ和對(duì)偶的?φ刻畫對(duì)多agent系統(tǒng)的認(rèn)知，其中，?φ表示在任意信息事件[2]之后，φ都會(huì)成立。隨后，Hans van Ditmarsch等將精化模態(tài)邏輯(refinement modal logic,RML)看作是FEL的抽象[3]，因此?算子表示對(duì)精化的量化，也稱為精化量詞，用以描述與所給的信息狀態(tài)相匹配的信息事件。

隨著研究的不斷深入，學(xué)者們逐漸意識(shí)到，在不同的模態(tài)邏輯下用結(jié)構(gòu)轉(zhuǎn)換來(lái)解釋精化量詞具有更廣泛的意義，由此，Laura Bozzelli等在Hans van Ditmarsch研究的基礎(chǔ)上，進(jìn)一步將精化量詞引入模態(tài)邏輯，并展開了相關(guān)的研究工作。精化與互模擬的區(qū)別在于前者只需滿足(back)條件,而對(duì)(forth)條件并沒(méi)有限制[4-5]。

文中將對(duì)精化關(guān)系加以層次的限制，進(jìn)一步探究n-精化關(guān)系(n-refinement)?；贚aura Bozzelli等的研究工作[6]，將著眼于n-精化與n-互模擬之間的轉(zhuǎn)換關(guān)系，提出相對(duì)化的概念，從而建立基于語(yǔ)義等價(jià)的從n-精化模態(tài)邏輯到n-互模擬量化邏輯的翻譯函數(shù)。

1 預(yù)備知識(shí)

令A(yù)表示有限的agent集合，P表示可數(shù)的命題變?cè)希硎咀匀粩?shù)集。用a,b,a',b',…表示A中的元素，并且用p,q,r,p',p'',…表示P中的元素。

下面參考n-互模擬[7]引入n-精化關(guān)系的概念。

定義1(n-精化，n-互模擬)：對(duì)任意B?A及模型M=(S,R,V)和M'=(S',R',V')，二元關(guān)系序列{Zi}i≤n是M和M'之間關(guān)于B的n-精化關(guān)系(n-refinement)，當(dāng)且僅當(dāng)Zn?…?Z0?S×S'且對(duì)任意(v,v')∈S×S'，a∈A-B，b∈A以及0≤i≤n，如下條件成立：

(atoms)如果vZ0v'，那么對(duì)于任意p∈P，v∈V(p)當(dāng)且僅當(dāng)v'∈V'(p)；

對(duì)于任一給定n∈及B?A，點(diǎn)模型上的二元關(guān)系定義如下：當(dāng)且僅當(dāng)M與M'之間存在關(guān)于B的n-精化關(guān)系{Zi}i≤n使得sZnt。亦采用記號(hào)說(shuō)明{Zi}i≤n是M與M'之間存在關(guān)于B的n-精化關(guān)系且sZnt。當(dāng)B={a}時(shí)，將表示為不難得證，對(duì)于任意n∈，本身是一個(gè)n-精化關(guān)系。

本節(jié)將給出n-精化模態(tài)邏輯的語(yǔ)法、語(yǔ)義及其可靠完備的公理系統(tǒng)。

2.1 語(yǔ)言及語(yǔ)義

定義2(n-精化模態(tài)邏輯語(yǔ)言L?n)：令A(yù)是一個(gè)有限agent集合，P是原子命題的可數(shù)集合，L?n公式由以下BNF范式定義，其中B?A，a∈A，p∈P且n∈。

φ::=p|

定義3(n-精化模態(tài)邏輯的語(yǔ)義)：公式L?n的可滿足性歸納定義如下：

Ms|=p當(dāng)且僅當(dāng)s∈VM(p)；

Ms|=φ當(dāng)且僅當(dāng)Ms|≠φ；

Ms|=φ∧ψ當(dāng)且僅當(dāng)Ms|=φ且Ms|=ψ；

定義4(n-互模擬量化邏輯語(yǔ)言L?n)：L?n公式可按以下BNF范式歸納定義：

φ::=p|

由命題1可知如下結(jié)論成立：

2.2 n-精化的語(yǔ)義操作

根據(jù)定義2可知，n-互模擬是n-精化關(guān)系，反之卻不成立。這一節(jié)研討n-互模擬關(guān)系和n-精化關(guān)系之間的聯(lián)系。

(1)S'?SM∪SN；

(2)對(duì)任意b∈A:

(3)V'?VM∪VN。

證明：類似引理1，令R''=RN，原子命題p在N'中SM域上為假，SN域上為真即可得證。

3 語(yǔ)言L?n到的翻譯

首先引入相對(duì)化的定義。

q(a,p)=q；

(φ∧ψ)(a,p)=φ(a,p)∧ψ(a,p)；

(□aφ)(a,p)=□a(p→φ(a,p))；

(□bφ)(a,p)=□b(p→φ(a,p))，其中b≠a；

證明：根據(jù)公式φ的結(jié)構(gòu)復(fù)雜度歸納證明。

對(duì)不同的原子命題關(guān)于不同agent進(jìn)行相對(duì)化與順序無(wú)關(guān)，下面給出具體驗(yàn)證過(guò)程。

證明：根據(jù)公式φ的結(jié)構(gòu)復(fù)雜度不難得證。

t(p)=p；

t(φ)=t(φ)；

t(φ∧ψ)=t(φ)∧t(ψ)；

t(□aφ)=□at(φ)；

下面給出含多個(gè)不同n-精化算子的L?n公式的翻譯。

例1：

命題4：給定點(diǎn)模型Ms，對(duì)于任意φ∈，均有Ms|=φ當(dāng)且僅當(dāng)Ms|=t(φ)。

證明：按照φ∈L?n的結(jié)構(gòu)復(fù)雜度證明。

4 結(jié)束語(yǔ)

目前，關(guān)于精化模態(tài)邏輯已經(jīng)有比較完善的研究結(jié)果，Hans等已經(jīng)給出了從精化關(guān)系到互模擬關(guān)系的轉(zhuǎn)換過(guò)程，由此RML語(yǔ)言翻譯成互模擬量化邏輯語(yǔ)言[11-12]，并將該結(jié)果應(yīng)用于RMLμ公理系統(tǒng)的可靠性證明中[12-13]。文中提出了n-精化關(guān)系的概念，基于n-互模擬和精化的定義[14]，給出n-精化的定義及其數(shù)學(xué)性質(zhì)。在n-精化的語(yǔ)義操作前提下，研究n-互模擬、n-精化關(guān)系之間的關(guān)系，因此提出了相對(duì)化[15]的概念，比較了相對(duì)化概念與標(biāo)準(zhǔn)相對(duì)化之間的區(qū)別與聯(lián)系。在此基礎(chǔ)上考察將n-精化模態(tài)邏輯語(yǔ)言翻譯成n-互模擬量化邏輯語(yǔ)言。未來(lái)的研究工作會(huì)將n-精化模態(tài)μ演算翻譯成n-互模擬量化語(yǔ)言，并探究n-模態(tài)μ演算公理系統(tǒng)[16]的可靠性與完備性。

參考文獻(xiàn)：

[1] VAN DITMARSCH H,FRENCH T,PINCHINAT S.Future event logic-axioms and complexity[C]//Seventh conference on advances in modal logic.[s.l.]:[s.n.],2010:77-99.

[2] VAN DITMARSCH H,FRENCH T.Simulation and information:quantifying over epistemic events[M]//Knowledge representation for agents and multi-agent systems.Berlin:Springer-Verlag,2009:51-65.

[4] BLACKBURN P, DE RIJKE M, VENEMA Y. Modal logic[M]//Cambridge tracts in theoretical computer science.Cambridge:Cambridge University Press,2001.

[5] D’AGOSTINO G,LENZI G.An axiomatization of bisimulation quantifiers via the μ-calculus[J].Theoretical Computer Science,2005,338(1-3):64-95.

[6] BOZZELLI L,VAN DITMARSCH H,FRENCH T,et al.Refinement modal logic[J].Information and Computation,2014,239:303-339.

[7] KUPKE C,KURZ A,VENEMA Y.Completeness of the finitary Moss logic[C]//Seventh conference on advances in modal logic.[s.l.]:[s.n.],2008:193-217.

[8] VENEMA Y.Lectures on the modal μ-calculus[D].Beijing:Renmin University in Beijing,2008.

[9] FRENCH T N.Bisimulation quantifiers for modal logics[D].Australia:University of Western Australia,2006.

[10] D’AGOSTINO G,HOLLENBERG M.Logical questions concerning the μ-calculus:interpolation,Lyndon andos-Tarski[J].Journal of Symbolic Logic,2000,65(1):310-332.

[11] CHISWELL I,HODGES W.Mathematical logic[M].[s.l.]:[s.n.],2007.

[12] HALES J.Refinement quantifiers for logics of belief and knowledge[D].Australia:University of Western Australia,2011.

[13] HALES J,FRENCH T,DAVIES R.Refinement quantified logics of knowledge[J].Electronic Notes in Theoretical Computer Science,2011,278:85-98.

[14] HALES J,FRENCH T,DAVIES R.Refinement quantified logics of knowledge and belief for multiple agents[C]//Seventh conference on advances in modal logic.[s.l.]:[s.n.],2012:317-338.

[15] 鈕 俊,曾國(guó)蓀,王 偉.綠色評(píng)價(jià)模型的互模擬等價(jià)及邏輯保持[J].計(jì)算機(jī)學(xué)報(bào),2013,36(5):967-976.

[16] 顏 鋒,田作威,嚴(yán)榴香.多態(tài)π演算的互模擬等價(jià)關(guān)系及其公理化[J].計(jì)算機(jī)工程與科學(xué),2010,32(10):131-134.