走进模态逻辑的互模拟

Bi-simulation Is Going into the Modal Logic

描述两个模型的模态等价性,同态显得太弱,同构又显得太强,寻找一个介于同态与同构之间的概念就导致了互模拟的产生。在模态逻辑中,互模拟沿着同态-强同态-有界态射-互模拟的轨迹而产生。在无穷模态语言的背景下或在像有穷的克里普克模型上,两个模型模态等价当且仅当它们是互模拟的。今天,互模拟在模态逻辑、集合论和计算机科学等领域中得到广泛的应用,显示了互模拟强大的理论价值和实践价值。

For characterizing the equivalence of two models,homomorphism is too weak and isomorphism is too strong,so it is necessary to look for an notion between homomorphism and isomorphism,which is now called bi-simulation.Bi-simulation was produced along homomorphism-strong homomorphism-bounded morphisms-bi-simulation in modal logic.In LM$ or in the class of image-finite Kripke models two models are modal equivalence if and only if they are bi-similar.Today,bi-simulations are widely used in modal logic,set theory and computer science,which shows their great value both in theories and in practices.