有关模拟理论的论文：互模拟理论的逻辑研究述评.doc

《有关模拟理论的论文：互模拟理论的逻辑研究述评.doc》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、有关模拟理论的论文：互模拟理论的逻辑研究述评在20世纪70年代前后，互模拟理论在许多领域被独立建立。自从范本特姆(VanBenthem)定理问世之后，互模拟被广泛地运用于模态逻辑的研究中，目前已成为模态逻辑模型论的一个核心概念;在集合论中，互模拟的研究不断向深度和广度扩展。当今，互模拟不断地被用到新的形式化理论中，这对于逻辑学，特别是哲学逻辑的进一步发展将起到极大的促进作用。一什么是互模拟从直观上讲，互模拟就是两个系统能够相互模仿对方，从而在观察者看来，它们是行为等价的。在20世纪70年代，人们在计算机科学、模态逻辑和集合论中大体上同时并且独立地发现了互模拟。经典的互

2、模拟概念定义在一个加标转换系统(LTS)上。互模拟令LTS二是两个有相同标号集的加标转换系统，如果下面的条件成立，那么一个非空二元关系Z二Wxw’被称为LTS和LTS’之间的一个互模拟关系(记作Z:LTS竺LTs‘):(i)如果wZw‘，并且Rawv，那么在W，中存在一个v’使得vZv’，并且Ra’w’v‘。(11)如果wZw‘，并且Ra’w‘v’，那么在W中存在一个v使得vzv’，并且Rawv。如果是LTS到LTS’的一个互模拟关系，并且wzw’，我们称w和w‘是互模拟的。!’:二互模拟理论研究概况互模

3、拟研究的开端可追溯到20世纪60年代后期计算机科学的研究，米尔纳(Milner)的工作最为突出，帕克(Park)在固定点理论的指导下，于1981年正式提出互模拟与互模拟证明方法。〔’)在计算机科学之外，互模拟在哲学逻辑和集合论等逻辑领域也得到持续而深人的研究。互模拟被广泛地运用于模态逻辑的研究中，目前已成为模态逻辑模型论的一个核心概念。范本特姆1976年把模型之间具有的p一态射有向关系扩充成一个模型间的对称关系，以p一关系为名引人互模拟概念，得出模态逻辑的互模拟不变性质，并进一步导出了“模态逻辑是一阶逻辑的互模拟不变部分”的结论(范本特姆刻画定理)。:’〕沃洛柯威茨(

4、walukiewicz)和贾宁(Janin)1996年把互模拟运用到一元二阶逻辑(MSO)，提出并且证明了林一演算是Mso互模拟不变的部分。!‘1这个定理首次把Mso、互模拟和林一演算三个概念联系起来。亨尼西(Henllessy)和米纳尔研究了互模拟与模态等价的关系问题，证明在像有穷的模型类上，两个状态互模拟当且仅当它们是模态等价的。!’l戈德布拉特(Goldblatt)提出了Hennessy一Milner类，它是互模拟与模态等价一致的模型类。像有穷的模型类就属于这样的类。白磊本(PatrickBlackbum)等证明了模态饱和的模型类和可数饱和的模型类也属于这一类。

5、胡能伯格(Hollenberg)讨论了与Hennessy-Milner类相关的许多概念，并且讨论了这些概念之间的联系，得出“像有穷的模型类恰好是所有极大Hennessy一Milner类的交”的结论。[6〕巴威斯(J.Barwise)和莫斯(L.MosS)1996年从另一角度研究了互模拟与模态等价的关系问题。他们把基本模态逻辑扩展成无穷模态逻辑ML二，并证明在无穷模态逻辑ML二中互模拟与模态等价性是一致的。「7〕帕特森(Ann。Patterson)研究了直觉主义命题逻辑的模型上的互模拟与语言等价的关系，得出直觉主义命题逻辑的两个有穷的、或者有穷的和主要过滤的、或者饱和的

6、克里普克(Kripke)模型是互模拟的当且仅当它们有相同的有效公式集。但是，如果这两个模型是像有穷的，这个结论不成立，这一点与模态逻辑中的情况不同。〔8)米斯拉(JayadewMisra)研究了互模拟理论本身的性质。他给出了互模拟和最大互模拟的特征，证明了最大互模拟是一个等价关系，并且是他所定义的函数F的最大固定点。「9〕互模拟的一些变体在模态逻辑中也得到研究。格布兰德(JeneGethrand)基于克里普克模型定义了互模拟与有界互模拟，给出了模态逻辑的非良基模型定义和知识结构定义，证明了知识结构可被看做a一互模拟的点模型类。{’0桑吉罗吉(Dav记。sangiors

7、i)提出了模拟等价性概念，给出最大模拟、最大互模拟、以及模拟等价性之间的几个关系，并基于css讨论了倒钩互模拟;[川刘奋荣在《偏好变化和信息过程》文稿中给出了赋值模型上的赋值互模拟和距离互模拟。互模拟的算法问题也得到持续的研究。霍皮罗福特(H叩croft)1971年给出了一个使加标转换系统状态的数量最小化的算法，它等价于确定一个集合相对于一个有穷函数集的稳定的最粗糙的划分问题;佩奇(Paige)、塔贾(Tarjan)和博尼(Bonic)1985年基于只存在一个函数的情况提出线性时间中的“正战略算法”:开始是单元素类，然后通过一系列步骤把两个或更多的类