I haven't previously thought about this, but I think words over a commutative monoid are equivalent to a vector of non-negative integers, at which point you hav

I haven't previously thought about this, but I think words over a commutative monoid are equivalent to a vector of non-negative integers, at which point you have vector addition systems, and I believe those are decidable, though still computationally incredibly hard: https://www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/ https://www.quantamagazine.org/an-easy-sounding-problem-yiel....