The equivalence problem for deterministic pushdown transducers into abelian groups

The equivalence problem for deterministic pushdown transducers with inputs in a free monoid X* and outputs in an abelian group H is shown to be decidable. The result is obtained by constructing a complete formal system for equivalent pairs of deterministic rational series on the variable alphabet associated with the dpdt M with coefficients in the monoid H-0 (the monoid obtained by adjoining a zero to the group H).