On the Coverability Problem for Constrained Multiset Rewriting
Parosh Aziz Abdulla, Giorgio Delzanno · 2006
We investigate model checking of a computation model called Constrained Multiset Rewriting Systems (CMRS). A CMRS operates on configurations which are multisets of monadic predicate symbols, each with an argument ranging over the natural numbers. The transition relation is defined by a finite set of rewriting rules which are conditioned by simple inequalities on variables and constants. This model is able to specify systems with an arbitrary number of components where the internal state of a component may contain values ranging over the natural numbers. In this paper we prove decidability of the coverability problem for CMRS. The algorithm is obtained by a non-trivial application of a methodology based on the theory of well- and better-quasi orderings. We report on using a prototype implementation to verify parameterized versions of a mutual exclusion and an authentication protocol.