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.