05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
9 results
Search Results
Item Open Access Computational and logical aspects of infinite monoids(2003) Lohrey, Markus; Diekert, Volker (Prof. Dr.)The present work contains a treatise of several computational and logical aspects of infinite monoids. The first chapter is devoted to the word problem for finitely generated monoids. In particular, the relationship between the the computational complexity of the word problem and the syntactical properties of monoid presentations is investigated. The second chapter studies Cayley-graphs of finitely generated monoids under a logical point of view. Cayley-graphs of groups play an important role in combinatorial group theory. We will study first-order and monadic second-order theories of Cayley-graphs for both groups and monoids. The third chapter deals with word equations over monoids. Using the graph product operation, which generalizes both the free and the direct product, we generalize the seminal decidability results of Makanin on free monoids and groups to larger classes of monoids.Item Open Access Existential and positive theories of equations in graph products(2001) Diekert, Volker; Lohrey, MarkusWe prove that the existential theory of equations with normalized rational constraints in a fixed graph product of finite monoids, free monoids, and free groups is PSPACE-complete. Under certain restrictions this result also holds if the graph product is part of the input. As the second main result we prove that the positive theory of equations with recognizable constraints in graph products of finite and free groups is decidable.Item Open Access Infinite state model checking of propositional dynamic logics(2006) Göller, Stefan; Lohrey, MarkusModel-checking problems for propositional dynamic logic (PDL) and its extension PDL$^\cap$ (which includes the intersection operator on programs) over various classes of infinite state systems (BPP, BPA, pushdown systems, prefix-recognizable systems) are studied. Precise upper and lower bounds are shown for the data/expression/combined complexity of these model-checking problems.Item Open Access Inverse monoids : decidability and complexity of algebraic questions(2005) Lohrey, Markus; Ondrusch, NicoleThis paper investigates the word problem for inverse monoids generated by a set A subject to relations of the form e=f, where e and f are both idempotents in the free inverse monoid generated by A. It is shown that for every fixed monoid of this form the word problem can be solved in polynomial time which solves an open problem of Margolis and Meakin. For the uniform word problem, where the presentation is part of the input, EXPTIME-completeness is shown. For the Cayley-graphs of these monoids, it is shown that the first-order theory with regular path predicates is decidable. Regular path predicates allow to state that there is a path from a node x to a node y that is labeled with a word from some regular language. As a corollary, the decidability of the generalized word problem is deduced. Finally, it is shown that the Cayley-graph of the free inverse monoid has an undecidable monadic second-order theory.Item Open Access Model checking hierarchical structures(2005) Lohrey, MarkusHierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems when input graphs are defined hierarchical. In this paper, the model-checking problem for first-order logic (FO), monadic second-order logic (MSO), and second-order logic (SO) on hierarchically defined input graphs is investigated. It is shown that in general these model-checking problems are exponentially harder than their non-hierarchical counterparts, where the input graphs are given explicitly. As a consequence, several new complete problems for the levels of the polynomial time hierarchy and the exponential time hierarchy are obtained. Based on classical results of Gaifman and Courcelle, two restrictions on the structure of hierarchical graph definitions that lead to more efficient model-checking algorithms are presented.Item Open Access First order and counting theories of omega-automatic structures(2005) Kuske, Dietrich; Lohrey, MarkusThe logic L(Q_u) extends first-order logic by a generalized form of counting quantifiers ("the number of elements satisfying ... belongs to the set C"). This logic is investigated for structures with an injective omega-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable (Blumensath, Grädel 2004). It is shown that, as in the case of automatic structures (Khoussainov, Rubin, Stephan 2004) also modulo-counting quantifiers as well as infinite cardinality quantifiers ("there are c many elements satisfying ...") lead to decidable theories. For a structure of bounded degree with injective omega-automatic presentation, the fragment of L(Q_u) that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (omega-automaticity and bounded degree) are necessary for this result to hold.Item Open Access Fixpoint logics on hierarchical structures(2005) Göller, Stefan; Lohrey, MarkusHierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems. In this paper, the model-checking problem for the modal $\mu$-calculus and (monadic) least fixpoint logic on hierarchically defined input graphs is investigated. In order to analyze the modal $\mu$-calculus, parity games on hierarchically defined input graphs are investigated. In most cases precise upper and lower complexity bounds are derived. A restriction on hierarchical graph definitions that leads to more efficient model-checking algorithms is presented.Item Open Access Complexity results for confluence problems(1999) Lohrey, MarkusWe study the complexity of the confluence problem for restricted kinds of semi-Thue systems, vector replacement systems and general trace rewriting systems. We prove that confluence for length-reducing semi-Thue systems is P-complete and that this complexity reduces to AC 1 in the monadic case (where all right-hand sides consist of at most one symbol). For length-reducing vector replacement systems we prove that the confluence problem is PSPACE-complete and that the complexity reduces to NP and P, respectively, for monadic vector replacement systems and special vector replacement systems (where all right-hand sides are empty), respectively. Finally we prove that for special trace rewriting systems, confluence can be decided in polynomial time and that the extended word problem for special trace rewriting systems is undecidable.Item Open Access The power word problem in graph products(2024) Lohrey, Markus; Stober, Florian; Weiß, ArminThe power word problem for a group Gasks whether an expression u1x1⋯unxn, where the uiare words over a finite set of generators of Gand the xibinary encoded integers, is equal to the identity of G. It is a restriction of the compressed word problem, where the input word is represented by a straight-line program (i.e., an algebraic circuit over G). We start by showing some easy results concerning the power word problem. In particular, the power word problem for a group Gis uNC1-many-one reducible to the power word problem for a finite-index subgroup of G. For our main result, we consider graph products of groups that do not have elements of order two. We show that the power word problem in a fixed such graph product is AC0-Turing-reducible to the word problem for the free group F2and the power word problems of the base groups. Furthermore, we look into the uniform power word problem in a graph product, where the dependence graph and the base groups are part of the input. Given a class of finitely generated groups Cwithout order two elements, the uniform power word problem in a graph product can be solved in AC0[C=LUPowWP(C)], where UPowWP(C)denotes the uniform power word problem for groups from the class C. As a consequence of our results, the uniform knapsack problem in right-angled Artin groups is NP-complete. The present paper is a combination of the two conference papers (Lohrey and Weiß 2019b, Stober and Weiß 2022a). In Stober and Weiß (2022a) our results on graph products were wrongly stated without the additional assumption that the base groups do not have elements of order two. In the present work we correct this mistake. While we strongly conjecture that the result as stated in Stober and Weiß (2022a) is true, our proof relies on this additional assumption.