05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
26 results
Search Results
Item Open Access Gleichungen mit regulären Randbedingungen über freien Gruppen(2000) Hagenah, Christian; Diekert, Volker (Prof. Dr.)Wir beweisen, daß das Erfüllbarkeitsproblem für Gleichungen mit regulären Randbedingungen über freien Gruppen PSPACE-vollständig ist. Wir zeigen auch, daß eine minimale Lösung einer solchen Gleichung höchstens eine doppelt exponentielle Länge hat und in 2-DEXPTIME berechnet werden kann. Wir reduzieren zuerst das Problem Gleichungen mit regulären Randbedingungen über einer freien Gruppen zu lösen auf das Problem Gleichungen mit regulären Randbedingungen über freien Monoiden mit einer Anti-Involution zu lösen. Anschließend stellen wir einen Algorithmus vor, der in PSPACE entscheidet, ob diese Gleichungen lösbar sind und einen Algorithmus, der in 2-DEXPTIME eine Lösung berechnet, wenn die Gleichung lösbar ist.Item Open Access On hierarchical search and preference-based routing in transportation networks(2023) Proissl, Claudius; Funke, Stefan (Prof. Dr.)In dieser Arbeit werden verschiedene Problemstellungen der Routenplanung in Transportnetzwerken behandelt.Item Open Access Automatic synthesis of distributed transition systems(2006) Stefanescu, Alin; Esparza, Javier (Prof. Dr.)This thesis investigates the synthesis problem for two classes of distributed transition systems: synchronous products and asynchronous automata. The underlying structure of these models consist of local automata synchronizing on common actions. The synthesis problem discussed is as follows: Given a global specification as a transition system TS and a distribution pattern D, find a distributed transition system over D whose global state space is equivalent' to TS. As criteria for the correctness of the (distributed) implementation vs. the specification (i.e., their equivalence') we use: transition system isomorphism, language equivalence, and bisimilarity respectively. In particular, the synthesis of asynchronous automata modulo language equivalence is a notoriously hard problem solved by Zielonka at the end of the 80s. One of the motivations behind our work was to bring this theory closer to practical applications. From the theoretical point of view, we conduct a detailed analysis of the synthesis problem for both models of distributed systems, look at effective algorithmic approaches and draw a map of computational complexity results. E.g., we provide several matching lower and upper complexity bounds for the distributed implementability problem. From the practical perspective, we provide prototype implementations for most of the synthesis algorithms discussed in the thesis. Moreover, we offer assistance when a given specification is not distributable by trying to modify this specification such that distributed synthesis can be applied. By using several heuristics to overcome the classical state space explosion, we are able to automatically generate small distributed algorithms for problems such as mutual exclusion.Item Open Access Formal language theory of logic fragments(2014) Lauser, Alexander; Diekert, Volker (Prof. Dr.)The present thesis consists of two parts. Based on syntactic closure axioms of formula sets, the first part gives a formal definition of logic fragments. It also shows the versatileness of this notion of logic fragments, inter alia, giving, C-variety descriptions of logic fragments and abstractly investigating the influence of certain predicates on the expressiveness of logic fragments. The second part considers two-variable first-order logic FO2. A combinatorial description in terms of so-called rankers is given for all full levels as well as all half levels of the quantifier alternation hierarchy of FO2 over the order predicate, both with and without the successor predicate. Also in the second part, effective algebraic criteria describing all full levels as well as all half levels of the quantifier alternation hierarchy of FO2 over several signatures are given, yielding in particular decidability of the definability problem.Item Open Access Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verteilten Systemen(2006) Schröter, Claus; Esparza, Javier (Prof. Dr.)Das Hauptproblem bei der automatischen Verifikation von verteilten Systemen unter Verwendung von Model-Checking-Verfahren besteht in der Zustandsraumexplosion der Ausgangssysteme. Dieses bedeutet, daß sogar die Spezifikation eines kleinen Systems oftmals einen großen Zustandsraum aufspannt, da dieser exponentiell in der Größe des Ausgangssystems wachsen kann. In der Vergangenheit wurden verschiedene Techniken vorgeschlagen, um diese Problematik in den Griff zu bekommen. Diese können klassifiziert werden in Techniken, die auf eine implizite, kompakte Repräsentation des gesamten Zustandsraums abzielen, zum Beispiel codiert als BDD, oder die unter Verwendung von Abstraktionen oder Halbordnungsreduktionen eine reduzierte Zustandsraumrepräsentation verwenden. Eine dritte Klasse von Techniken stützt sich auf die Halbordnungssicht auf nebenläufige Berechnungen, und Systemzustände werden hier implizit durch die Verwendung azyklischer Petrinetze repräsentiert. Sehr populär darunter ist die Technik von McMillan zur Erzeugung endlicher, vollständiger Präfixe von Petrinetzentfaltungen. Das Ziel dieser Arbeit besteht darin, effiziente Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verschiedenen Petrinetzklassen zu analysieren, zu erweitern, zu implementieren und experimentell zu vergleichen. Eine der Hauptfragestellungen auf dem Gebiet der automatischen Verifikation untersucht die Erreichbarkeit von Systemzuständen, da viele Sicherheitseigenschaften eines Systems auf einfache Erreichbarkeitsfragen zurückgeführt werden können. Als typisches Beispiel sei hier die Eigenschaft zum wechselseitigen Ausschluß von nebenläufigen Prozessen erwähnt. In dieser Arbeit werden vier Verfahren betrachtet, die das Erreichbarkeitsproblem für 1-sichere Petrinetze unter Verwendung von Entfaltungspräfixen exakt lösen. Es werden zwei Halbentscheidungsverfahren betrachtet, die das Erreichbarkeitsproblem für 1-sichere Petrinetze unter Verwendung von Techniken der linearen Programmierung zu lösen versuchen. Die Verfahren werden anhand von experimentellen Ergebnissen miteinander verglichen, und es wird eine Empfehlung hergeleitet, welche Verfahren für praktische Belange geeignet zu sein scheinen. Es wird gezeigt, daß das PSPACE-vollständige Erreichbarkeitsproblem für 1-sichere Petrinetze in ein (möglicherweise exponentiell größeres) NP-vollständiges Problem überführt werden kann, sofern Entfaltungstechniken eingesetzt werden. Eine weitere wichtige Fragestellung auf dem Gebiet der automatischen Verifikation beschäftigt sich mit dem Nachweis von Sicherheits- und Lebendigkeitseigenschaften, die in Form von temporalen Logiken wie beispielsweise CTL oder LTL formuliert werden. Es werden Reduktionsregeln für den Nachweis von LTL-X-Eigenschaften betrachtet, die in zwei Kategorien eingeteilt werden können: Regeln, die lineare Programmierung unter Verwendung von Invarianten oder impliziten Stellen einsetzen, und Regeln, die lokale Netzreduktionen betrachten. Es wird gezeigt, daß die Bedingungen für die Anwendbarkeit einiger lokaler Netzreduktionen abgeschwächt werden können, sofern man LTL-X-Eigenschaften mit einem Verfahren von Esparza und Heljanko nachweist. Anhand von experimentellen Ergebnissen wird gezeigt, daß die Verifikationszeit für eine LTL-X-Eigenschaft eines Systems signifikant verringert werden kann, sofern dieses mit den vorgeschlagenen Reduktionsregeln vorverarbeitet wird. Schließlich wird der von Esparza und Heljanko vorgestellte entfaltungsbasierte Ansatz zum Nachweis von LTL-X-Eigenschaften 1-sicherer Petrinetze auf eine höhere Petrinetzklasse übertragen. Anhand von experimentellen Ergebnissen wird der in dieser Arbeit vorgestellte Ansatz mit dem Ansatz von Esparza und Heljanko sowie dem Model-Checker SPIN verglichen. Die Ergebnisse zeigen, daß der in dieser Arbeit verwendete Model-Checker dem Model-Checker von Esparza und Heljanko in allen Beispielen, und SPIN gegenüber in einigen Beispielen überlegen ist.Item Open Access On the complexity of conjugacy in amalgamated products and HNN extensions(2015) Weiß, Armin; Diekert, Volker (Prof. Dr. rer. nat. habil.)This thesis deals with the conjugacy problem in classes of groups which can be written as HNN extension or amalgamated product. The conjugacy problem is one of the fundamental problems in algorithmic group theory which were introduced by Max Dehn in 1911. It poses the question whether two group elements given as words over a fixed set of generators are conjugate. Thus, it is a generalization of the word problem, which asks whether some input word represents the identity. Both, word and conjugacy problem, are undecidable in general. In this thesis, we consider not only decidability, but also complexity of conjugacy. We consider fundamental groups of finite graphs of groups as defined by Serre - a generalization of both HNN extensions and amalgamated products. Another crucial concept for us are strongly generic algorithms - a formalization of algorithms which work for "most" inputs. The following are our main results: The elements of an HNN extension which cannot be conjugated into the base group form a strongly generic set if and only if both inclusions of the associated subgroup into the base group are not surjective. For amalgamated products we prove an analogous result. Following a construction by Stillwell, we derive some undecidability results for the conjugacy problem in HNN extensions with free (abelian) base groups. Next, we show that conjugacy is decidable if all associated subgroups are cyclic or if the base group is abelian and there is only one stable letter. Moreover, in a fundamental group of a graph of groups with free abelian vertex groups, conjugacy is strongly generically in P. Moreover, we consider the case where all edge groups are finite: If conjugacy can be decided in time T(N) in the vertex groups, then it can be decided in time O(log N * T(N)) in the fundamental group under some reasonable assumptions on T (here, N is the length of the input). We also derive some basic transfer results for circuit complexity in the same class of groups. Furthermore, we examine the conjugacy problem of generalized Baumslag-Solitar groups. Our main results are: the conjugacy problem in solvable Baumslag-Solitar groups is TC0-complete, and in arbitrary generalized Baumslag-Solitar groups it can be decided in LOGDCFL. The uniform conjugacy problem for generalized Baumslag-Solitar groups is hard for EXPSPACE. Finally, we deal with the conjugacy problem in the Baumslag group, an HNN extension of the Baumslag-Solitar group BS12. The Baumslag group has a non-elementary Dehn function, and thus, for a long time, it was considered to have a very hard word problem, until Miaskikov, Ushakov, and Won showed that the word problem, indeed, is in P by introducing a new data structure, the so-called power circuits. We follow their approach and show that the conjugacy problem is strongly generically in P. We conjecture that there is no polynomial time algorithm which works for all inputs, because the divisibility problem in power circuits can be reduced to this conjugacy problem. Also, we prove that the comparison problem in power circuits is complete for P under logspace reductions.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 Formal language theory of hairpin formations(2011) Kopecki, Steffen; Diekert, Volker (Prof. Dr. rer. nat. habil.)The (bounded) hairpin completion, the hairpin lengthening, and their iterated versions are operations on formal languages which have been inspired by the hairpin formation in DNA biochemistry. In this paper we discuss the hairpin formations from a language theoretic point of view. The hairpin completion of a formal language has been defined in 2006. In the first paper on this topic it has been shown that the hairpin completion of a regular language is not necessarily regular but always linear context-free. In the same paper the open problem was stated, if it is decidable, whether the hairpin completion of a regular language is regular. We solved this problem positively in 2009. Here, we prove that the problem is NL-complete and we present an algorithm whose time complexity is bounded by a polynomial of degree 8. As a by-product of our technique to prove the complexities, we obtain that the hairpin completion of a regular language is actually an unambiguous linear context-free language. In addition, we provide results concerning language classes within the regular languages. We show that if the hairpin completion of an aperiodic (i.e., star-free) language is regular, then the hairpin completion is aperiodic, too. The same is true for the language class induced by the variety LDA. The hairpin lengthening is a variant of the hairpin completion which has been investigated first in 2010. The hairpin lengthening of a regular language seems to behave quite similar to the hairpin completion: It is not necessarily regular but linear context-free. We prove, however, that the hairpin lengthening of a regular language may be an inherent ambiguous linear language. We also consider the problem if it is decidable, whether the hairpin lengthening of a regular language is regular, but we are only able to prove decidability for the one-sided case of hairpin lengthening. (The one-sided case is closer to biochemistry, yet the two-sided case is more interesting from a theoretic point of view). The bounded hairpin completion can be seen as a weaker variant of the hairpin completion. It is well-known that all language classes in the Chomsky hierarchy are closed under bounded hairpin completion and that context-free, context-sensitive, and recursively enumerable languages are closed under iterated bounded hairpin completion. In 2009 it was asked in literature, whether the regular languages are closed under iterated bounded hairpin completion as well. We solve this question by presenting a more general result. We give an effective representation for the iterated bounded hairpin completion which uses union, intersection with regular sets, and concatenation with regular. Thus, all lan- guage classes which are (effectively) closed under these basic operations are also (effectively) closed under iterated bounded hairpin completion. This applies to all classes in the Chomsky hierarchy and to all usual complexity classes. Furthermore, we give an exponential lower and upper bound for the size of non-deterministic finite automata accepting the iterated bounded hairpin completion of a regular language. The iterated (unbounded) hairpin completion of a regular language is known to be context-sensitive and it may be not context-free. However, it is was not known whether the iterated hairpin completion of a singleton (or finite language) is always regular or context-free. This was stated as an open problem in 2008. In contrast to the previous questions this one has a negative answer. We give an example of a singleton whose iterated hairpin completion is not context-free.Item Open Access Hierarchische Graphen zur Wegesuche(2000) Buchholz, Friedhelm; Claus, Volker (Prof. Dr.)In dieser Arbeit wird ein Zwei-Phasenmodell zur effizienten Entfernungsberechnung in gewichteten Graphen untersucht. Bekannte Anwendungsgebiete sind Verkehrsinformationssyteme, VLSI Design, Verteiltes Rechnen und geometrische und parallele Algorithmen. In einer Preprocessing-Phase wird zu einem Graphen ein Hierarchischer Graph (HG) konstruiert, der in der Online-Phase zur Entfernungsberechnung eingesetzt wird. Es werden die Laufzeit (T) der Preprocessing-Phase, die Groesse (S) des HG'en und die Laufzeit (Q) der Online-Phase untersucht. Zwei kontraere Modellierungsansaetze werden vorgestellt: Geeignete Knoten und ein rekursives Separationskonzept. Das Konzept mit Geeigneten Knoten wird auf Levelgraphen verallgemeinert und es wird gezeigt, dass die Berechnung einer minimalen Geeigneten Knotenmenge NP-vollstaendig ist. Die Approximation bzgl. der Groesse der Geeigneten Knotenmenge kann bis auf einen logarithmischen Faktor und bezueglich des Umgebungsabstands bis auf einen konstanten Faktor in polynomieller Laufzeit durchgefuehrt werden. Im Falle von planaren Graphen wird mittels eines erweiterten Separationskonzepts (Ideen von Lingas 1990 und von Didjev 1996 werden kombiniert) gezeigt, dass HG'en von fast linearer Groesse genuegen, um Q in O(n {1.5} log 3 n) zu gewaehrleisten. Dieses Resultat ist modulo logarithmischer Faktoren optimal. Ausserdem wird ein neuer Parameter 'Separatorweite' fuer Graphen eingefuehrt und es wird konstruktiv gezeigt, dass die Separatorweite unabhaengig von der Baumweite ist, aber hoechstens um einen logarithmischen Faktor von der Baumweite abweicht. Am Beispiel wird gezeigt, dass eine logarithmische Abweichung auftreten kann.Item Open Access Contraction hierarchies: theory and applications(2022) Rupp, Tobias; Funke, Stefan (Prof. Dr.)Contraction Hierarchies describes a technique that enormously accelerates the calculation of shortest paths on road networks in practice. In the first part of this thesis, this acceleration is analyzed theoretically. For this purpose, we introduce the graph family of lightheaded grids. On one hand, light-headed grids have realistic properties as planarity and occur in real world road networks. On the other hand, their generic structure makes them suitable for theoretical analysis. We prove a lower bound Ω( n) for the average query phase of contraction hierarchies on lightheaded grids. At the cost of more disk space, hub labels is another technique which enables even quicker answering of shortest path queries than contraction hierarchies. For hub labels, we prove that the average hub label size of a node is in Ω( n) on lightheaded grids with the same idea as in the previous proof. Then we develop this proof idea even further into a schema which is able to compute instance-based lower bounds for both contraction hierarchies and hub labels on any arbitrary given graph. For some graph families such as balanced ternary trees, we show that this schema yields tight bounds, i.e. the lower bounds matches a concrete contraction hierarchy and hub labeling. In previous contributions concerning upper bounds, it was believed that it is meaningful to consider only explored nodes to upper bound the query time. For example, it was proven for one proposed contraction strategy based on separators, that during query time of contraction hierarchies, only sublinear many nodes are explored on average for a wide family of graphs which includes lightheaded grids. For lightheaded grids, we prove that this strategy yields linear many edges to be explored on average, therefore showing that considering only the number of explored nodes is not sufficient. We also show that it is not the contraction hierarchy framework which is necessarily flawed but the proposed strategy by giving another strategy for which only sublinear many edges need to be explored on average. In the second part of this thesis, contraction hierarchies are adapted to fit other purposes than answering short paths queries only. First, we show how trajectories, i.e. movement of individuals on the road network, can be stored efficiently if the contraction hierarchy data structure is present. When describing the compression process of raw trajectory data, we also prove that the compressed presentation is unique. Having the data compressed will also be beneficial for answering retrieval queries which ask for all trajectories intersecting a given space-time cube. We describe how to augment the contraction hierarchy data structure further to answer such queries quicker than state-of-the-art approaches. Interestingly, contraction hierarchies can also be instrumentalized to visualize graph simplifications 9as it was already demonstrated in the URAN framework. However, the URAN framework had some shortcomings which we address. We ensure that a simplified graph retains its original silhouette better and avoids some topological inconsistencies. Moreover, we apply similar techniques to visualize trajectory data sets within our framework PATHFINDERVIS which is also able to provide different flavors of visualization including heat-map based ones.
- «
- 1 (current)
- 2
- 3
- »