Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs

A distributed model for the π-calculus is presented in terms of Place/Transition Petri nets with inhibitor arcs (PTI for short). Such a class of nets is equipped with a step and a causal semantics, hence allowing to study non-interleaving semantics for the π-calculus. We show the correctness of the semantics by proving that the interleaving semantics induced by the PTI semantics is fully abstract with respect to the interleaving early semantics originally defined in terms of labelled transition systems. We also argue the impossibility to define reasonable distributed semantics that preserve the intended non-interleaving semantics if we simply use Place/Transition nets without inhibitor arcs. Some decidability results (notably, the satisfaction of linear time μ-calculus formulae) are presented for the subclass of the π-calculus generating finite PTI nets.