用Pi^+演算表示带抑止弧的Petri网

Describing Petri Net with Inhibitor Arcs Using Pi Calaulus

Pi演算和Petri网是常用的两种形式化建模技术,关于他们之间的相互表达问题已经引起了人们的关注。主要目的是研究如何用Pi演算表示一种扩展的Petri网——带抑制弧的Petri网。为了能够表示Petri网的静态及动态结构,首先介绍了具有同步同信原语的Pi+演算,但是这种扩展无法表示抑制位置无穷的Petri网,因此又提出了优先原语,并通过例子说明了优先原语的作用。

Pi calculus and Petri net are two formal modeling technologies,the problem about how to express each other has gained attentions.Aim of this paper is studying how to express Petri net with inhibitor arcs using pi calculus.To express static and dynamic structure of Petri net,Pi+ calculus with multi-primitive synchronized communication mechanism is introduced.But Petri net with infinity inhibitor place don't be depicted using this extend,so prior primitive is given and its action is explained through examples.