资源描述：
《互模拟的含义_特征及主要应用》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、重庆理工大学学报(社会科学)2010年第24卷第2期逻辑学与科学方法论JournalofChongqingUniversityofTechnology(SocialScience)Vol24No.22010互模拟的含义、特征及主要应用姚从军(南开大学哲学系,天津300071)摘要:给出互模拟精确且具有概括性定义(B),给出并证明了互模拟的5个特征,最后给出最大互模拟~定义,证明了~是一个等价关系,进一步证明了~是R中(B)的最大固定点。概括了互模拟在模态逻辑和并发系统中的非凡的应用价值,并提出了某些尚待解决的问题。互模拟具有美好的发展前景和极大的发展空间。关键词:互模拟;
2、模态逻辑;等价关系;固定点;并发系统中图分类号:B81文献标识码:A文章编号:1674-8425(2010)02-0030-04一、什么叫互模拟一个标号转换系统是一个带有标号边的有向图(可能是无穷的)。标号不必不同。每个标号称为一个转换。结点通常被称为状态。图1一个标号转换系统上的互模拟关系大体说来,如果从一个结点开始的每条有穷例子在图2中,我们能够证明下面的对是最路径,存在一条从另一个结点开始的具有相同标大互模拟的:号的路径,那么两个结点是互模拟的。在许多系(a,A),(a,A∀),(b,B),(c,C),(A,A∀)统中,互模拟状态是不可区分的,因为从一个状态开
3、始的每一步都从另一个状态开始的类似步与之匹配。如果我们把项与结点联系起来,把转换与项重写规则联系起来,我们能够使用互模拟证明项的相等性。注意,非形式描述蕴涵着一个结点与自身是互模拟的,现在没有形式定义支持。图2两个标号转换系统之间的互模拟关系例子在图1中,我们可以证明(a,A)和互模拟定义一个互模拟R是满足下面条件(b,B)是互模拟的。很容易证明(b,B)是互模拟的一个转换系统上对称性的二元关系。的因为存在一个从b和B到同一个目标的同一转已知pRq换。并且(a,A)是互模拟的是因为(1)从A和a<:pp∀(q∀#qq∀∃p∀Rq∀)>(B)经过转换标号0到达互模拟结
4、点,并且(2)它们经过转换标号1到达同一个结点。这里p和q是结点,是一个标号,pq表示具有标号的从p到q的一条边。收稿日期:2009-11-30基金项目:2008年国家社科基金超集、互模拟以及在模态逻辑、计算机科学中的作用研究资助项目(08BZX049)。作者简介:姚从军(1971!),男,湖北随州人,博士,研究方向:现代逻辑。姚从军:互模拟的含义、特征及主要应用31注意对于定义(B)证明:对所有,i假设Ri是互模拟。假设p%R不必然是自反的。空关系是一个互Riq。那么,对某个,jpRjq。我们证明(B).模拟[1]。!p∀:pp∀,q∀#qq∀∃p∀Rjq∀R
5、不一定是传递的。在图3中,我们有pRq,(by(B))qRr,但是pRr(p∀Rr∀)不成立。R={(p,q)(q,r)}!p∀:pp∀,q∀#qq∀∃p∀%Riq∀(根据关系的并定义)&(P5)假设转换系统是确定性的,那么互模拟的交是互模拟。证明:首先,我们解释在一般的情况下,互模拟在交下不封闭。考虑图4。这里,R和S是互模拟的,并且图3非传递的互模拟关系p(R∋S)q。然而,p∀(R∋S)q∀和p∀(R∋S)q(都不这个互模拟不是传递的。成立。我们有pp∀。但是不存在r满足qr要求R是等价关系也许很有用。存在一个∃p∀(R∋S)r。缺点:互模拟在并运算下封闭,但是
6、等价关系在并假设转换系统是确定的,也就是,下不必封闭。考虑等价关系R和S,其中pRq,pp∀∃pp(!p∀=p(qSr。那么,pR%Sq,qR%Sr,但是pR%Sr不成立。因为R%S中找不到一个关系使得pr具有该关系。二、互模拟的性质&(P1)恒等关系id是一个互模拟,这里对所有p,pidp成立。证明:从互模拟定义(B)&(P2)已知R是一个互模拟,所以R-1也是互模拟。证明:从互模拟对称性,R-1=R图4在交下不封闭的互模拟关系&(P3)互模拟关系的合成也是互模拟。我们证明互模拟在交运算下封闭。令p(R∋令R、S是互模拟,假设p(R.S)q。从关系合S)q,也就是p
7、Rq和pSq。那么,对于p∀:pp∀成的定义可得,存在一个r使得pRr并且rSq。那么,!q∀#qq∀∃p∀Rq∀和q(#qq(∃p∀Sq((据pRq和pSq)pp∀!(r∀#rr∀∃p∀Rr∀)(从pRr和(B))!q∀#qq∀∃p∀Rq∀∃p∀Sq∀(确定性条件蕴涵q∀=q()rr∀!(q∀#qq∀∃r∀Sq∀)(从rRs和(B))!q∀#qq∀∃p∀(R∋S)q∀(关系交的定义)pp∀!(q∀,r∀#qq∀∃p∀Rr∀∃r∀Sq∀)(从上面二者)
