n-互模擬及其相關性質

南京航空航天大學計算機科學與技術學院 施曉靜

n-互模擬及其相關性質

南京航空航天大學計算機科學與技術學院 施曉靜

n-互模擬理論在許多領域都被獨立建立。在計算機科學領域中，如果系統之間存在n-互模擬關系，那么在n-步以內的路徑，系統之間的行為均可相互模擬。本文將探究n-互模擬關系的相關性質。

n-互模擬；等價關系；向前條件；向后條件

1.引言

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

2.n-互模擬

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

圖1 向前條件與向后條件

3.結束語

本文主要給出了n-互模擬的定義，并給出了其具體圖例，證明了其是等價關系的相關數學性質。根據這些研究成果，可以進一步探究n-互模擬關系與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.