Zusammenfassung
We introduce the notion of idempotent variables for studying equations in inverse monoids. It is proved that it is decidable in singly exponential time (DEX-PTIME) whether a system of equations in idempotent variables over a free inverse monoid has a solution. Moreover the problem becomes hard for DEXPTIME, as soon as the quotient group of the free inverse monoid has rank at least two. The upper ...
Zusammenfassung
We introduce the notion of idempotent variables for studying equations in inverse monoids. It is proved that it is decidable in singly exponential time (DEX-PTIME) whether a system of equations in idempotent variables over a free inverse monoid has a solution. Moreover the problem becomes hard for DEXPTIME, as soon as the quotient group of the free inverse monoid has rank at least two. The upper bound is proved by a direct reduction to solve language equations with one-sided concatenation and a known complexity result by Baader and Narendran (J. Symb. Comput. 31, 277-305 2001). For the lower bound we show hardness for a restricted class of language equations. Decidability for systems of typed equations over a free inverse monoid with one irreducible variable and at least one unbalanced equation is proved with the same complexity upper-bound. Our results improve known complexity bounds by Deis et al. (IJAC 17, 761-795 2007). Our results also apply to larger families of equations where no decidability has been previously known. The lower bound confirms a conjecture made in the conference version of this paper.
Altmetric