Article ID Journal Published Year Pages File Type
426575 Information and Computation 2012 20 Pages PDF
Abstract

We combine two of the existing approaches to the study of concurrency by means of multiset rewriting: multiset rewriting with existential quantification (MSR) and constrained multiset rewriting. We obtain ν-MSR, where we rewrite multisets of atomic formulae, in which terms can only be pure names, where some names can be restricted. We consider the subclass of depth-bounded ν-MSR, for which the interdependence of names is bounded. We prove that they are strictly Well Structured Transition Systems, so that coverability, termination and boundedness are all decidable for depth-bounded ν-MSR. This allows us to obtain new verification results for several formalisms with name binding that can be encoded within ν-MSR, namely polyadic ν-PN (Petri nets with tuples of names as tokens), the π-calculus, MSR or Mobile Ambients.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, ,