05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
7 results
Search Results
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.