On the relationship between π-calculus and finite place/transition petri nets

Abstract

We clarify the relationship between π-calculus and finite p/t Petri nets. The first insight is that the concurrency view to processes taken in [Eng96, AM02, BG09] and the structural view in [Mey09] are orthogonal. This allows us to define a new concurrency p/t net semantics that can be combined with the structural semantics in [Mey09]. The result is a more expressive mixed semantics, which translates precisely the so-called mixed-bounded processes into finite p/t nets. Technically, the translation relies on typing of restricted names. As second main result we show that mixed-bounded processes form the borderline to finite p/t nets. For processes just beyond this class reachability becomes undecidable and so no faithful translation into finite p/t nets exists. © 2009 Springer Berlin Heidelberg.