n-互模擬及其相關(guān)性質(zhì)

南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院 施曉靜

n-互模擬及其相關(guān)性質(zhì)

南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院 施曉靜

n-互模擬理論在許多領(lǐng)域都被獨立建立。在計算機科學(xué)領(lǐng)域中，如果系統(tǒng)之間存在n-互模擬關(guān)系，那么在n-步以內(nèi)的路徑，系統(tǒng)之間的行為均可相互模擬。本文將探究n-互模擬關(guān)系的相關(guān)性質(zhì)。

n-互模擬；等價關(guān)系；向前條件；向后條件

1.引言

直觀上講，互模擬就是兩個系統(tǒng)能夠相互模仿對方，從而從觀察者的角度講，在某種程度上，它們是行為等價的?；ツM被廣泛地運用于模態(tài)邏輯的研究中，比如用它去分析其他類型模態(tài)邏輯的表達(dá)力；在模型檢測中互模擬用來收縮模型，同時還保持模型的語義等等。目前，學(xué)術(shù)界對于互模擬關(guān)系和n-互模擬關(guān)系展開了大量的研究工作，已有的結(jié)論是，互模擬是一種n-互模擬關(guān)系，反之卻不成立。那么，n-互模擬作為精化的有限近似，將在模型檢測中，更有利于縮減檢測的狀態(tài)空間。

2.n-互模擬

例2（向前條件與向后條件）下圖示中所說明的n-互模擬關(guān)系的向前條件和向后條件。實線箭頭表示可達(dá)關(guān)系，虛線箭頭表示存在著相應(yīng)與之匹配的可達(dá)關(guān)系，點狀連接線表示-連接。向前條件說的是，在已知且的情況下，總可以找到一個使得并且。下圖的右半部分說明了向后條件。 □

圖1 向前條件與向后條件

3.結(jié)束語

本文主要給出了n-互模擬的定義，并給出了其具體圖例，證明了其是等價關(guān)系的相關(guān)數(shù)學(xué)性質(zhì)。根據(jù)這些研究成果，可以進(jìn)一步探究n-互模擬關(guān)系與n-精化關(guān)系的聯(lián)系。

[1]Blackburn P,De Rijke M,Venema Y.Modal Logic:Graph.Darst[M].Cambridge University Press,2002.

[2]Aucher G.Characterizing updates in dynamic epistemic logic[C].Twelfth International Conference on the Principles of Knowledge Representation and Reasoning.2010.

[3]Aucher G.DEL-sequents for regression and epistemic planning[J].Journal of Applied Non-Classical Logics,2012,22(4):337-367.

[4]Balbiani P,Baltag A,Van Ditmarsch H,et al.Knowable as known after an announcement[J].The Review of Symbolic Logic,2008,1(03):305-334.

[5]Baltag A,Moss L S,Solecki S.The logic of public announcements,common knowledge,and private suspicions[M].Readings in Formal Epistemology.Springer International Publishing,2016:773-812.

[6]Bílková M,Palmigiano A,Venema Y.Proof systems for the coalgebraic cover modality[J].Advances in modal logic,2008(7):1-21.