Solving Trace Equations Using Lexicographical Normal Forms

摘要

Very recently, the second author showed that the question whether an equation over a trace monoid has a solution or not is decidable [11,12]. In the original proof this question is reduced to the solvability of word equations with constraints, by induction on the size of the commutation relation. In the present paper we give anotherp proof of this result using lexicographical normal forms. Our method is a direct reduction of a trace equation system to a word equation system with regular constraints, using a new result on lexicographical normal forms.