05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
Search Results
Item Open Access Reachability analysis of multithreaded software with asynchronous communication(2005) Bouajjani, Ahmed; Esparza, Javier; Schwoon, Stefan; Strejcek, JanWe introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations.Item Open Access Reguläre Häufigkeitsberechnungen(2005) Austinat, Holger; Diekert, Volker (Prof. Dr.)Die vorliegende Arbeit beschäftigt sich mit Häufigkeitsberechnungen, einem rekursionstheoretischen Begriff, der in den 60er Jahren von Rose eingeführt wurde. Eine Funktion f ist berechenbar mit Frequenz m/n, wenn es einen Algorithmus gibt, der für je n verschiedene Eingaben n Ausgabewerte berechnet, von denen mindestens m mit den zugehörigen Funktionswerten von f übereinstimmen. Eine erste natürliche Fragestellung war: gibt es nicht-berechenbare Funktionen, die mit einer Frequenz nahe 1 berechnet werden können? Trakhtenbrot beantwortete diese Frage 1963 negativ, indem er zeigte, dass eine Funktion mit Frequenz echt größer als 1/2 bereits berechenbar im herkömmlichen Sinne ist. Andererseits gibt es überabzählbar viele Funktionen, die sich mit Frequenz 1/2 berechnen lassen. Also ist dieses Ergebnis optimal. Die Forschung auf diesem Gebiet intensivierte sich daraufhin: Wissenschaftler wie Dëgtev, Kinber und Trakhtenbrot selbst (in den 70er und 80er Jahren) und Beigel, Gasarch, Hinrichs, Kummer, Stephan, Tantau und Wechsung (ab den 90er Jahren) beschäftigten sich mit verschiedenen Aspekten von Häufigkeitsberechnungen und verwandten Berechenbarkeitsbegriffen. In der vorliegenden Arbeit beschäftigen wir uns vorwiegend mit regulären Häufigkeitsberechnungen, also solchen, die von endlichen Automaten vorgenommen werden können. Kinber untersuchte diesen Aspekt als erster im Jahre 1976 und behauptete, dass sich Trakhtenbrots Resultat auf endliche Automaten überträgt. Sein folgerte dies aus einem allgemeineren Resultats über separierbare Sprachen, das sich allerdings als falsch herausstellte (ein Gegenbeispiel wurde 2002 von Tantau angegeben). (Zwei disjunkte Sprachen A und B heißen separierbar, wenn ein Algorithmus alle Wörter aus A akzeptiert und alle Wörter aus B ablehnt). Die Frage, ob das Analogon von Trakhtenbrots Resultat für endliche Automaten gilt, stellte sich also von neuem. Diese Dissertation enthält folgende Ergebnisse. In Kapitel 2 geben wir zwei Beweise für Trakhtenbrots Resultat an. Zunächst präsentieren wir seinen Originalbeweis, um dann einen neuen kombinatorischen Beweis zu geben, der einen großen Vorteil besitzt: er erlaubt die Übertragung des Ergebnisses auf endliche Automaten. Zwei kleinere Resultate beschließen dieses Kapitel: der Nachweis, dass es überabzählbar viele nicht häufigkeitsberechenbare Sprachen gibt, und eine Darstellung des Zusammenhangs von Häufigkeitsberechnungen und sog. mulit-selektiven Mengen. In Kapitel 3 arbeiten wir den Fehler in Kinbers Beweis über separierbare Sprachen heraus und geben ein konkretes Gegenbeispiel an. Dann untersuchen wir die Separierbarkeit von sog. Pfad- und Anti-Pfadsprachen, die wie folgt definiert sind: sei alpha ein unendliches Wort über dem Alphabet { 0, 1 }; dann ist A(alpha) die Menge der endlichen Präfixe von alpha, und B(alpha) die Menge der Wörter von A(alpha), bei denen das letzte Bit negiert wurde. Wir zeigen, dass A(alpha) und B(alpha) genau dann separiert werden können, wenn die 1-Positionen von alpha berechnet werden können. Andererseits gibt es überabzählbar viele alpha, für die A(alpha) und B(alpha) mit Frequenz 1/2 berechnet werden können. Wenn (ab drei Eingaben) nur ein Fehler zugelassen ist, dann sind A(alpha) und B(alpha) bereits rekursiv. Dieses Ergebnis überträgt sich auch auf endliche Automaten. Zum Abschluss dieses Kapitels zeigen wir, dass sich Kinbers Vermutung (dass Trakhtenbrots Resultat auch für Sprachen gilt, die durch endliche Automaten separiert werden können) nicht retten lässt: für jede Konstante q < 1 gibt es Werte 1 <= m < n mit m/n > q und ein alpha derart, dass A(alpha) und B(alpha) durch endliche Automaten mit Frequenz m/n separiert werden können, jedoch nicht rekursiv separierbar sind. In Kapitel 4 untersuchen wir verschiedene Aspekte regulärer Häufigkeitsberechnungen. Wir zeigen zunächst, dass sich Trakhtenbrots Resultat auf endliche Automaten überträgt, indem wir den neuen Beweis aus Kapitel 2 nochmals genauer betrachten. Anschließend zeigen wir, dass aperiodische Automaten, die Häufigkeitsberechnungen durchführen, nur aperiodische reguläre Sprachen berechnen können (aperiodische Sprachen entsprechen sternfreien Sprachen). Dann beweisen wir ein sog. Iterationskriterium, das vergleichbar mit dem bekannten Pumping-Lemma für reguläre Sprachen ist und uns für viele konkrete Beispielsprachen den Nachweis erlaubt, dass diese nicht häufigkeitsberechenbar sind. Im letzten Teil untersuchen wir dann Abschlusseigenschaften der Klasse der regulär häufigkeitsberechenbaren Sprachen: wir zeigen, dass sie eine boolesche Algebra bilden, jedoch nicht unter Spiegelung abgeschlossen sind. Darüberhinaus ist die Vereinigung zweier Sprachen, die mit Frequenz 1/n erkennbar sind, in der Regel nicht 1/n-erkennbar. Wir beweisen eine untere Schranke, die sehr nah an der besten bekannten oberen Schranke liegt.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 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 Ring-Isomorphie-Probleme und das Faktorisieren großer Zahlen(2005) Staiger, StefanDie Diplomarbeit ist eine Ausarbeitung und Weiterführung der aktuellen Forschung von Neeraj Kayal und Nitin Saxena. Diese haben das algorithmische Studium von Fragen rund um Ringe begonnen. Die Diplomarbeit präsentiert die hierbei entstandenen Algorithmen und komplexitätstheoretischen Überlegungen in ausführlicher und verständlicher Weise. Behandelt werden beispielsweise die Fragen, ob zwei Ringe isomorph sind, wie viele Automorphismen sie haben und wie man Iso- und Automorphismen berechnen kann. Hierzu werden eine Reihe mathematischer Grundlagen erläutert. Darüber hinaus leitet die Diplomarbeit neue Ergebnisse zu endlichen Ringen her und korrigiert einen Fehler von Kayal und Saxena. Ferner werden die Ring-Probleme in Beziehung gesetzt zu den bekannten Problemen der Graph-Isomorphie und des Faktorisierens großer Zahlen. Die Arbeit präsentiert außerdem einen Überblick über die aktuellen Faktorisierungsverfahren und schließt mit einer Reihe noch offener Fragen, die als Grundlage für weitere Forschung dienen können.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 Ambiguity functions of context-free grammars and languages(2005) Wich, Klaus; Diekert, Volker (Prof. Dr.)This thesis investigates the relationship between the ambiguity functions for context-free grammars and for context-free languages. It also examines which functions are ambiguity functions and how different ambiguity classes relate to each other. The results can be applied to generalise known results on sequential and parallel parsing of context-free grammars. To understand the main results we define some notions briefly: The ambiguity of a word with respect to a context-free grammar is the number of its derivation trees. The ambiguity function of a context-free grammar maps an integer n to the maximal ambiguity of a word whose length is bounded by n. A context-free language L is f-ambiguous if f is the ambiguity function of some context-free grammar generating L and, roughly speaking, no context-free grammar generating L has a substantially lower ambiguity. A function is an inherent ambiguity function if there is an f-ambiguous context-free language. A homomorphism which maps a symbol either to itself or to the empty word is called a projection. A symbol a is called bounded in a language L if there is a constant c such that no word in L has more than c occurrences of the symbol a. A projection is a bounded contraction for a language L if it erases only symbols which are bounded in L. The main results are: 1. The set of ambiguity functions for cycle-free context-free grammars and the set of inherent ambiguity functions coincide. 2. A technical statement which implies the following two facts: 2.1. The class of context-free languages with polynomially bounded ambiguity is the closure of the class of unambiguous context-free languages under bounded contractions. 2.2. Each reduced cycle-free context-free grammar G is either exponentially ambiguous or its ambiguity is bounded by a polynomial which can be computed from G. (2.2. was already part of the authors Diploma thesis, but the new proof yields in many cases a better polynomial (a polynomial with a lower degree), but never a worse polynomial.) 3. For each computable divergent total non-decreasing function f there is a divergent ambiguity function g such that g(n) is lower than or equal to f(n) for each positive integer n. In fact, the same ambiguity functions occur for the generation of rational trace languages over special independence alphabets. (A rational trace language T is generated by a regular (word) language R if T is the set of traces which are represented by the words in R. The ambiguity of a trace t is the number of representatives in R. It is now straightforward to define the ambiguity function for the generation of T by R.) In addition the thesis contains generalisations for known results on sequential and parallel parsing of context-free grammars. In particular, the thesis considers the (sequential) Earley parsing time of context-free grammars with sublinear ambiguity functions (known to exist due to result 3). Moreover it is shown that each reduced context-free grammars with a polynomially bounded ambiguity can be parsed in logarithmic time on a CREW-PRAM. This is an immediate consequence of 2.1. and a known result for the parallel parsing time of unambiguous context-free grammars.