Reachability in unions of commutative rewriting systems is decidable

Abstract

We consider commutative string rewriting systems (Vector Addition Systems, Petri nets), i.e., string rewriting systems in which all pairs of letters commute. We are interested in reachability: given a rewriting system R and words v and w, can v be rewritten to w by applying rules from R? A famous result states that reachability is decidable for commutative string rewriting systems. We show that reachability is decidable for a union of two such systems as well. We obtain, as a special case, that if h : U → S and g : U → T are homomorphisms of commutative monoids, then their pushout has a decidable word problem. Finally, we show that, given commutative monoids U, S and T satisfying S ∩ T = U, it is decidable whether there exists a monoid M such that S ∪ T ⊆ M; we also show that the problem remains decidable if we require M to be commutative, too. © Springer-Verlag Berlin Heidelberg 2007.