×

zbMATH — the first resource for mathematics

Existential and positive theories of equations in graph products. (English) Zbl 1067.03017
In this article it is proved that, for a fixed graph product \(\mathbb P\) of finite monoids, free monoids, and free groups, the existential (i.e., sentences in prenex normal form without universal quantifiers) theory of equations can be decided in PSPACE. Moreover, when the equations have normalized rational (NRAT\((\mathbb P)\)) constraints, the problem becomes PSPACE-complete. Another main result states that, for graph products of finite and free groups, the positive (i.e., sentences without negations) theory of equations with recognizible (REC\((\mathbb G)\)) constraints is decidable. These results continue the stream of research on decidability of theories of equations on monoids and groups started by G. S. Makanin [Mat. Sb., Nov. Ser. 103(145), 147–236 (1977; Zbl 0371.20047)]. The results in this paper are based on the main result of V. Diekert and A. Muscholl [Lect. Notes Comput. Sci. 2076, 543–554 (2001; Zbl 0986.20036)] on existential theories of equations in trace monoids with involution. This result is used within the underlying trace monoid with involution of the graph product. It is proved that, for an existential sentence \(\phi\) with constraints in NRAT\((\mathbb P)\), there exist an existential sentence \(\phi'\) such that \(\phi\) holds in \(\mathbb P\) if and only if \(\phi'\) holds in the underlying monoid with involution. In this reduction, a specific confluent trace rewriting systems is used. The decidability of the positive theory of equations with constraints in REC\((\mathbb G)\), where \(\mathbb G\) is a graph product of finite and free groups, is proved in two steps. Firstly, it is proved that it possible to restrict the investigation to graph products of a particular type, and, secondly, the positive sentences with constraints in REC are reduced to existential sentences with constraints in NRAT. The result then follows by the first result.

MSC:
03B25 Decidability of theories and sets of sentences
03D15 Complexity of computation (including implicit computational complexity)
20M05 Free semigroups, generators and relations, word problems
20F10 Word problems, other decision problems, connections with logic and automata (group-theoretic aspects)
68Q25 Analysis of algorithms and problem complexity
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q42 Grammars and rewriting systems
PDF BibTeX Cite
Full Text: DOI