上海交通大学学报

上海交通大学学报（自然版） ›› 2011, Vol. 45 ›› Issue (07): 980-984.

• 自动化技术、计算机技术 • 上一篇    下一篇

有界Petri网的进程演算表达

董振华a,b，董笑菊a，b   

  1. (上海交通大学 a.计算机科学与工程系BASICS实验室； b.智能计算与智能系统教育部微软重点实验室， 上海 200240)
  • 收稿日期:2010-07-18 出版日期:2011-07-29 发布日期:2011-07-29
  • 基金资助:

    国家自然科学基金资助项目(60873034)，上海市自然基金资助项目(10ZR1416800)

Representing Bounded Petri Nets by Process Calculi

 DONG  Zhen-Hua-a, b , DONG  Xiao-Ju-a, b   

  1. (a.BASICS, Department of Computer Science； b.MOEMS Key Laboratory for Intelligent Computing and Intelligent Systems， Shanghai Jiaotong University, Shanghai 200240, China)
  • Received:2010-07-18 Online:2011-07-29 Published:2011-07-29

摘要： 为了进一步探讨Petri网与进程演算的关系，给出了一种使用进程演算模型(CCS)表示有界Petri网的方法.对于任意的有界Place/Transition网，可以用该方法构建一个与之相对应的有限进程.并且证明了所得进程与原网之间满足操作一致性和观察一致性.同时，证明了该方法在网的标号互模拟上满足完全抽象性.

关键词: Petri网, 进程演算, 编码

Abstract: A formal encoding method was given to represent bounded Petri nets by CCS which is one kind model of process calculi for researching the relationship between Petri nets and process calculi. A Place/Transition net could be encoded to a finite process by this method. The process and the original net satisfy the operational and observational correspondence. In this view, they have the same behaviors. It shows that the encoding method is fully abstract with respect to the labeled bisimulation, which is an equivalence relation between nets.

Key words: Petri nets, process calculi, encoding

中图分类号: