Volker Diekert, Artur Jeż, Manfred Kufleitner, Alexander Thumm
Let [Formula: see text] be a free partially commutative monoid with involution and [Formula: see text] its quotient group (for example, a right-angled Artin or Coxeter group). We show that for any system of word equations over [Formula: see text] with recognizable constraints, the solution set — in [Formula: see text] or in [Formula: see text] — is an EDT0L language. It is given by an NFA [Formula: see text] recognizing endomorphisms over some extended monoid. Furthermore, if the input size is [Formula: see text], then [Formula: see text] can be constructed effectively by an [Formula: see text]-transducer. As a consequence, both Satisfiability (whether the system admits a solution) and Finiteness (whether the solution set is infinite) are decidable in [Formula: see text]. For a natural subclass of constraints, we conjecture that these problems are [Formula: see text]-complete.