On the theory of one-step rewriting in trace monoids

We prove that the first-order theory of the one-step rewriting relation associated with a trace rewriting system is decidable and give a nonelementary lower bound for the complexity. The decidability extends known results on semi-Thue systems but our proofs use new methods; these new methods yield the decidability of local properties expressed in first-order logic augmented by modulo-counting quantifiers. Using the main decidability result, we describe a class of trace rewriting systems for which the confluence problem is decidable. The complete proofs can be found in the Technical Report [14].