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

For two given ω-terms α and β, the word problem for ω-terms over a variety V asks whether α = β in all monoids in V. We show that the word problem for ω-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 ω-terms (this property is also known as ω-reducibility). In particular, the separation problem for the corners of the Trotter-Weil Hierarchy is decidable.