We clarify the relationship between picalc and finite p/t Petri nets. The first insight is that the concurrency view to processes taken in cite{Engelfriet1996,AmadioMeyssonnier2002,BusiGorrieri2009} and the structural view in cite{Meyer2009StructStat} are orthogonal. This allows us to define a new concurrency p/t net semantics that can be combined with the structural semantics in cite{Meyer2009StructStat}. 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.
R. Meyer, R. Gorrieri (2009). On the Relationship between π-Calculus and Finite Place/Transition Petri Nets. HEIDELBERG : Springer-Verlag.
On the Relationship between π-Calculus and Finite Place/Transition Petri Nets
GORRIERI, ROBERTO
2009
Abstract
We clarify the relationship between picalc and finite p/t Petri nets. The first insight is that the concurrency view to processes taken in cite{Engelfriet1996,AmadioMeyssonnier2002,BusiGorrieri2009} and the structural view in cite{Meyer2009StructStat} are orthogonal. This allows us to define a new concurrency p/t net semantics that can be combined with the structural semantics in cite{Meyer2009StructStat}. 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
