n-精化與n-互模擬之間相關問題的研究

施曉靜，張晉津

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

0 引 言

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

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

隨著研究的不斷深入，學者們逐漸意識到，在不同的模態邏輯下用結構轉換來解釋精化量詞具有更廣泛的意義，由此，Laura Bozzelli等在Hans van Ditmarsch研究的基礎上，進一步將精化量詞引入模態邏輯，并展開了相關的研究工作。精化與互模擬的區別在于前者只需滿足(back)條件,而對(forth)條件并沒有限制[4-5]。

文中將對精化關系加以層次的限制，進一步探究n-精化關系(n-refinement)。基于Laura Bozzelli等的研究工作[6]，將著眼于n-精化與n-互模擬之間的轉換關系，提出相對化的概念，從而建立基于語義等價的從n-精化模態邏輯到n-互模擬量化邏輯的翻譯函數。

1 預備知識

令A表示有限的agent集合，P表示可數的命題變元集合，表示自然數集。用a,b,a',b',…表示A中的元素，并且用p,q,r,p',p'',…表示P中的元素。

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

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

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

對于任一給定n∈及B?A，點模型上的二元關系定義如下：當且僅當M與M'之間存在關于B的n-精化關系{Zi}i≤n使得sZnt。亦采用記號說明{Zi}i≤n是M與M'之間存在關于B的n-精化關系且sZnt。當B={a}時，將表示為不難得證，對于任意n∈，本身是一個n-精化關系。

本節將給出n-精化模態邏輯的語法、語義及其可靠完備的公理系統。

2.1 語言及語義

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

φ::=p|

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

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

Ms|=φ當且僅當Ms|≠φ；

Ms|=φ∧ψ當且僅當Ms|=φ且Ms|=ψ；

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

φ::=p|

由命題1可知如下結論成立：

2.2 n-精化的語義操作

根據定義2可知，n-互模擬是n-精化關系，反之卻不成立。這一節研討n-互模擬關系和n-精化關系之間的聯系。

(1)S'?SM∪SN；

(2)對任意b∈A:

(3)V'?VM∪VN。

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

3 語言L?n到的翻譯

首先引入相對化的定義。

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；

證明：根據公式φ的結構復雜度歸納證明。

對不同的原子命題關于不同agent進行相對化與順序無關，下面給出具體驗證過程。

證明：根據公式φ的結構復雜度不難得證。

t(p)=p；

t(φ)=t(φ)；

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

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

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

例1：

命題4：給定點模型Ms，對于任意φ∈，均有Ms|=φ當且僅當Ms|=t(φ)。

證明：按照φ∈L?n的結構復雜度證明。

4 結束語

目前，關于精化模態邏輯已經有比較完善的研究結果，Hans等已經給出了從精化關系到互模擬關系的轉換過程，由此RML語言翻譯成互模擬量化邏輯語言[11-12]，并將該結果應用于RMLμ公理系統的可靠性證明中[12-13]。文中提出了n-精化關系的概念，基于n-互模擬和精化的定義[14]，給出n-精化的定義及其數學性質。在n-精化的語義操作前提下，研究n-互模擬、n-精化關系之間的關系，因此提出了相對化[15]的概念，比較了相對化概念與標準相對化之間的區別與聯系。在此基礎上考察將n-精化模態邏輯語言翻譯成n-互模擬量化邏輯語言。未來的研究工作會將n-精化模態μ演算翻譯成n-互模擬量化語言，并探究n-模態μ演算公理系統[16]的可靠性與完備性。

參考文獻：

[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] 鈕 俊,曾國蓀,王 偉.綠色評價模型的互模擬等價及邏輯保持[J].計算機學報,2013,36(5):967-976.

[16] 顏 鋒,田作威,嚴榴香.多態π演算的互模擬等價關系及其公理化[J].計算機工程與科學,2010,32(10):131-134.