Constraint Multiset Rewriting

The framework called MSR is based on multiset rewriting systems defined over first-order atomic formulas and it has been introduced by Cervesato et al. [11] for the formal specification of cryptographic protocols. In [14], the basic formalism (i.e., without existential quantification) has been extended to allow for the specification of relations over data variable using constraints, i.e. a logic language interpreted over a fixed domain. Multiset rewriting rules allow one to locally model rendez-vous and internal actions of processes, and constraints to symbolically represent the relation between the data of different processes, thus achieving a clear separation between process structure and data paths. This formalism can be viewed as a first-order extension of Petri Nets in which tokens carry along structured data. We will call the resulting formalism $\mbox{MSR($\ {\mathscr C} $)}$. First of all, we introduce the notion of constraint system.