Reachability is Decidable for Ground AC Rewrite Systems

The reachability problem for ground associative-commutative (AC) rewrite systems is decidable. We show that ground AC rewrite systems are equivalent to Process Rewrite Systems (PRS) for which reachability is decidable [4]. However, the decidability proofs for PRS are cumbersome and thus we present a simpler and more readable proof in the framework of ground AC rewrite systems. Moreover, we show decidability of reachability of states with certain properties and decidability of the boundedness problem. 1 Introduction Ground AC systems are obtained by combining ground rewrite systems (i.e. rewrite systems without substitution) with the associative and commutative laws for a symbol denoted by +. These laws are applied as symmetric rewrite rules, i.e. from right to left and vice-versa. The reachability problem for ground AC systems has already been considered by A. Deruyver and R. Gilleron in [2] who proved that it is decidable under some restrictions: the + symbols can occur only at the r..