The Word Problem for Omega-Terms over the Trotter-Weil Hierarchy

For two given $\omega$-terms $\alpha$ and $\beta$, the word problem for $\omega$-terms over a variety $\boldsymbol{\mathrm{V}}$ asks whether $\alpha=\beta$ in all monoids in $\boldsymbol{\mathrm{V}}$. We show that the word problem for $\omega$-terms over each level of the Trotter-Weil Hierarchy is decidable. More precisely, for every fixed variety in the Trotter-Weil Hierarchy, our approach yields an algorithm in nondeterministic logarithmic space (NL). In addition, we provide deterministic polynomial time algorithms which are more efficient than straightforward translations of the NL-algorithms. As an application of our results, we show that separability by the so-called corners of the Trotter-Weil Hierarchy is witnessed by $\omega$-terms (this property is also known as $\omega$-reducibility). In particular, the separation problem for the corners of the Trotter-Weil Hierarchy is decidable.