第28卷 第1期 2005年1月计 算 机 学 报 CHINESEJOURNAL OF COMPUTERSVol. 28 No. 1 Jan. 20052网的强互模拟等价曹木亮1) ,2)吴智铭1)1)(上海交通大学电子信息学院 上海 200030)2)(桂林陆军学院 桂林 541002)收稿日期:2003206213;修改稿收到日期:2004210210.本课题得到国家自然科学基金(60074011 ,70071017)资助.曹木亮,男,1966年生,博士研究生,副教授,主要研究方向为Petri网、 2演算、 密码学. E2mail :ml-cao 163.com.吴智铭,男,1937年生,教授,博士生导师,主要研究方向为离散事件系统、 混杂动态系统以及它们在工业中的应用.摘 要 该文建立了2网的强互模拟等价关系,对2网的结构作了进一步的研究.2网是一类新型的基于2演算语义的模块化高级Petri网,是对两类并发模型Petri网和2演算的有效结合,它的并发语义既是 “真正并发” 的又是 “交互” 的.2网的强互模拟等价是针对2网的交互性并发语义的,是基于2网的标号操作语义规则,并直接用2网作为计算单元来实现的互模拟计算,使得2网的行为能够从动态和静态两方面得到考察.该文证明了对于任意的一个2网N,都存在一个2进程P,在2网与2演算系统等价映射 下,( N)与N是强互模拟的这一重要的结论.关键词 2网;2演算;标号操作规则;强互模拟等价中图法分类号TP301The Strong Bisimilarity on the2NetsCAO Mu2Liang1) ,2) WU Zhi2Ming1)1)( School of Electronic and Information Engineering , Shanghai Jiao Tong University , Shanghai 200030)2)( Guilin Military Institute , Guilin 541002)Abstract This paper builds up the strong bisimilarity on2nets.2net is a new modular high2level Petrinet based on the semantics of the2calculus which combines the advantages of Petri net and the2calculus.The concurrency semantics of2nets is not only“true concurrency”but also“interleaving”. The strong bisim2ilarity on2nets addresses the study of its interleaving semantics. Differing from the other approach of strongbisimilarity on standard Petri nets , the bisimilarity on2nets is based on the labeling operational rules of2nets , and computed straightly by2nets themselves instead of markings. It is shown that for any2net ,there is a processPsuch that( P)is bisimilarity toN, whereis the system equivalence from2calcu2lus to2nets.Keywords 2net ;2calculus; labeling operational rules; strong bisimilarity1 引 言在文献1 ,我们构造了一类新型的基于2演 算2,3语义的模块化的高级Petri网,称之为2网, 并建立了2网的标号操作语义规则,这些语义规则 有效地将2网变迁的激发变成了可操作的代数运算.本文中我们将建立2网的强互模拟等价关系, 进一步从 “迹”(或者说是从变迁激发序列)的角度来讨论2网的结构问题.因为2网是将Petri网和2 演算这两类并发模型进行有机的结合而得到的一种 并发机制,所以2网的并发语义不仅是 “真正并发” 的,同时也是 “交互” 的,其 “真正并发” 的语义已经从2 网是一类特殊的高级Petri网得到了直观的体现,而 “交 1995-2005 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved.2计 算 机 学 报2005年 1995-2005 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved.31期曹木亮等:2网的强互模拟等价 1995-2005 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved.4计 算 机 学 报2005年 1995-2005 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved.51期曹木亮等:2网的强互模拟等价 1995-2005 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved.6计 算 机 学 报2005年 1995-2005 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved.参考文献1Cao Mu2Liang , Wu Zhi2Ming.2nets , A high2level modular Petri netbased on the semantics of the2calculus. Journal of Shanghai JiaotongUniversity , 2004 , 38(1) : 5258(in Chinese)(曹木亮,吴智铭.一类新型的模块化高级Petri网 2网.上海交通大学学报, 2004 , 38(1) : 5258)2Milner R. , ParrowJ. , Walker D. . A calculusof mobile processes(partand) . Information and Computation , 1992 ,100(1) :1773Milner R. . Mobile Communication and2Calculus. Springer2PrenticeHall , 19994Fu Yu2Xi. Meta model of concurrent computation I. graph model. Jour2nal of Shanghai Jiaotong University , 2000 ,34 (6) :723726 (in Chi2nese)(傅育熙.并发计算的元模型.上海交通大学学报,2000 , 34(6) :723736)5Sangiorgi D. . A theoryof bisimulation for the2calculus. In: Proceed2ings of the CONCUR93 ,Lecture Notes in Computer Science 715 ,Springer2Verlag , 19936Olderog E2R. . Strong bisimilarity on nets: A new concept fot comparingnet semantics. In: Proceedings of the Rex School/workshop on LinerTime ,Branching Time and Partial Order in Logics and Models for Con2currency ,Noordwijkerhout , 1989 , 5495737Nielsen M. ,Winskel G. . Petri nets and bisimulation. Theoretical Com2puter Science , 1996 , 153: 21324471期曹木亮等:2网的强互模拟等价 1995-2005 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved.CAO Mu2Liang , born in 1966 , Ph.D. candidate , associate professor.His re2search interests include Petri nets , pi2calcu2lus , cryptography etc.WU Zhi2Ming , born in 1937 , professor , Ph. D. supervisor.His research interests include discrete event systems , hybrid dynam2ic systems and their industrial application etc.BackgroundIn 1993 , R.Milner indicated in his Turing AwardLecture that :One line of development that links the algebraic concurrency endeav2or and the already existing and very fruitful work of Petri on Petrinets has become rather promising and yet difficult because the con2ceptual basis in the two cases doesnt line up perfectly. In fact , thefield of linking the two approaches has become enormously rich in thelast twenty years. There are plentiful and substantial results aboutfinding the relation between CCS and Petri nets. But since R.Milnerproposed the2calculus in 1989 , just only two researchers havetried to combine these two concurrent theories , the2calculus andPetri nets. They presented different schemes to solve this problem.But both of them did not solve the problem essentially. Now the au2thors of this paper constitute a n