π-网的强互模拟等价  

The Strong Bisimilarity on the π-Nets

作　　者：曹木亮[1] 吴智铭[1] 

机构地区：[1]上海交通大学电子信息学院

出　　处：《计算机学报》2005年第1期1-8,共8页Chinese Journal of Computers

基　　金：国家自然科学基金 (60 0 740 11;70 0 710 17)资助 .

摘　　要：该文建立了π 网的强互模拟等价关系 ,对π 网的结构作了进一步的研究 .π 网是一类新型的基于π 演算语义的模块化高级Petri网 ,是对两类并发模型Petri网和π 演算的有效结合 ,它的并发语义既是“真正并发”的又是“交互”的 .π 网的强互模拟等价是针对π 网的交互性并发语义的 ,是基于π 网的标号操作语义规则 ,并直接用π 网作为计算单元来实现的互模拟计算 ,使得π 网的行为能够从动态和静态两方面得到考察 .该文证明了对于任意的一个π 网N ,都存在一个π 进程P ,在π 网与π 演算系统等价映射Ψ下 ,Ψ(N)与N是强互模拟的这一重要的结论 .This paper builds up the strong bisimilarity on π nets. π net is a new modular high level Petri net based on the semantics of the π calculus which combines the advantages of Petri net and the π calculus. The concurrency semantics of π nets is not only “true concurrency” but also “interleaving”. The strong bisimilarity on π nets addresses the study of its interleaving semantics. Differing from the other approach of strong bisimilarity on standard Petri nets, the bisimilarity on π nets is based on the labeling operational rules of π nets, and computed straightly by π nets themselves instead of markings. It is shown that for any π net, there is a process P such that Ψ(P) is bisimilarity to N , where Ψ is the system equivalence from π calculus to π nets.

关 键 词：π-网 Π-演算 标号操作规则 强互模拟等价 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]