Depth Boundedness in Multiset Rewriting Systems with Name Binding

In this paper we consider nu-MSR, a formalism that combines the two main existing approaches for multiset rewriting, namely MSR and CMRS. In nu-MSR we rewrite multisets of atomic formulae, in which some names may be restricted. nu-MSR are Turing complete. In particular, a very straightforward encoding of pi-calculus process can be done. Moreover, p nu-PN, an extension of Petri nets in which tokens are tuples of pure names, are equivalent to nu-MSR. We know that the monadic subclass of nu-MSR is a Well Structured Transition System. Here we prove that depth-bounded nu-MSR, that is, nu-MSR systems for which the interdependance of names is bounded, are also Well Structured, by following the analogous steps to those followed by R. Meyer in the case of the pi-calculus. As a corollary, also depth-bounded p nu-PN are WSTS, so that coverability is decidable for them.