有界Petri网的进程演算表达

Representing Bounded Petri Nets by Process Calculi

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

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.