Multiset Rewriting: A Semantic Framework for Concurrency with Name Binding

We revise multiset rewriting with name binding, by combining the two main existing approaches to the study of concurrency by means of multiset rewriting: multiset rewriting with existential quantification and constrained multiset rewriting. We obtain nu-MSRs, where we rewrite multisets of atomic formulae, in which some names may be restricted. We prove that nu-MSRs are equivalent to a class of Petri nets in which tokens are tuples of pure names, called p nu-APNs. Then we encode pi-calculus processes into nu-MSRs in a very direct way, that preserves the topology of bound names, by using the concept of derivatives of a pi-calculus process. Finally, we discuss how the recent results on decidable subclasses of the pi-calculus are independent of the particular reaction rule of the pi-calculus, so that they can be obtained in the more general framework of nu-MSRs. Thus, those results carry over not only to the pi-calculus, but to any other formalism that can be encoded within it, as p nu-APNs.