Trace monoids are well-studied objects in computer science where they serve as a basic algebraic tool for analyzing concurrent systems. The question whether the existential theory of trace equations is decidable has been solved positively in 1996. Free partially commutative groups (graph groups) generalize trace monoids in the sense that every element has an inverse. In this paper we show that the existential theory of equations over graph groups is decidable, too. Our decision procedure is non-elementary, but if a certain graph theoretical parameter is viewed as a constant, then we obtain a PSPACE-completeness result. Restricting ourselves to trace monoids we still obtain a better complexity result, as it was known previously.
展开▼
