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.
On the Relationship between π-Calculus and Finite Place/Transition Petri Nets / R. Meyer; R. Gorrieri. - STAMPA. - 5710:(2009), pp. 463-480. (Intervento presentato al convegno CONCUR 2009 - Concurrency Theory, 20th International Conference tenutosi a Bologna nel 1-4- Settembre 2009).
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.
