05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6

Browse

Filters

Settings

End date: 2022Subject: search.filters.subject.004Institute: search.filters.UBSInstitut.Institut für Formale Methoden der InformatikPublication Type: search.filters.UBSTyp.Dissertation

Search Results

Now showing 1 - 10 of 25
  • Thumbnail Image
    ItemOpen 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.
  • Thumbnail Image
    ItemOpen 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.
  • Thumbnail Image
    ItemOpen 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.
  • Thumbnail Image
    ItemOpen 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.
  • Thumbnail Image
    ItemOpen 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.
  • Thumbnail Image
    ItemOpen Access
    Algorithms for vehicle navigation
    (2012) Storandt, Sabine; Funke, Stefan (Prof. Dr.)
    Nowadays, navigation systems are integral parts of most cars. They allow the user to drive to a preselected destination on the shortest or quickest path by giving turn-by-turn directions. To fulfil this task the navigation system must be aware of the current position of the vehicle at any time, and has to compute the optimal route to the destination on that basis. Both of these subproblems have to be solved frequently, because the navigation system must react immediately if the vehicle leaves the precomputed route or the optimal path changes e.g. due to traffic jams. Therefore solving these tasks efficiently is crucial for safe and precise navigation. In this thesis we first described a fully autonomous localization scheme based on the shape of the driven trajectory, which provides very accurately the position of the vehicle in the street network. In the second part we investigated route planning for electric vehicle, describing efficient algorithms which allow for retrieving paths with low energy consumption in a fraction of a second on large street networks.
  • Thumbnail Image
    ItemOpen Access
    Logical fragments for Mazurkiewicz traces : expressive power and algebraic characterizations
    (2006) Kufleitner, Manfred; Diekert, Volker (Prof. Dr.)
    Mazurkiewicz trace are a model for concurrency. They can be seen as a generalization of words by introducing partial commutation between specific letters. Several logical and language-theoretic characterizations of the variety of monoids DA are known for words. We show which of them also hold for traces and which of them do not hold. An important tool for this task are Ehrenfeucht-Fraisse games. For several logical fragments, we introduce characterizations in terms of these games. They are used to separate logical fragments over traces that have the same expressive power over words. An essential property is, whether one can express concurrency within a fragment or not.
  • Thumbnail Image
    ItemOpen Access
    Improved algorithms for map rendering and route planning
    (2020) Mendel, Thomas; Funke, Stefan (Prof. Dr.-Ing.)
    In dieser Arbeit werden verschiedene Teilbereiche der Kartendarstellung und der Wegefindung betrachtet. Der erste Teil beschäftigt sich mit Grenzvereinfachung und Gebietsbeschriftung. Der zweite Teil stellt ein beschleunigtes Verfahren zur Berechnung kürzester Wege vor.
  • Thumbnail Image
    ItemOpen Access
    Similarity search with set intersection as a distance measure
    (2010) Hoffmann, Benjamin Sascha; Diekert, Volker (Prof. Dr.)
    This thesis deals with a fundamental algorithmic problem. Given a database of sets and a query set, we want to determine a set from the database that has a maximal intersection with the query set. It is allowed to preprocess the database so that queries can be answered efficiently. We solve the approximate version of this problem. We investigate two randomized input models which are derived from real inputs. We present a deterministic algorithm for each of them. Under the assumption that the database and the query set follow one of these models, the corresponding algorithm determines with high probability a set from the database that has no maximal intersection with the query set, but an intersection that achieves a large proportion of the maximal size. Depending on the model, the query time is either quasi-linear in the sum of the database size and the number of different elements from all sets, or it is polylogarithmic in the database size. Thus, both algorithms are significantly faster than a naive algorithm intersecting the query set with each single database set.
  • Thumbnail Image
    ItemOpen Access
    Labeling interactive maps
    (2020) Krumpe, Filip; Funke, Stefan (Prof. Dr.)
    Navigationssysteme, beziehungsweise digitale Kartenapps, haben sich zu alltäglichen Begleitern entwickelt. Waren digitale Karten vor einem Jahrzehnt ein wertvolles Gut - Updates für Navigationssysteme wurden für viel Geld verkauft- sind sie heute durch die Verbreitung von Google Maps und Co. eine Selbstverständlichkeit. Neben der Verfügbarkeit und der Möglichkeit einfacher Updates, ermöglichen digitale Karten eine einfache, intuitive Interaktion. Das Zoomen, Verschieben und Drehen des Kartenausschnitts zum Erkunden von Details und der Ausrichtung in Blickrichtung des Nutzers, sind wohlbekannte Funktionen. Letzteres ist vor allem bei Navigationssystemen zentral. Dort wird die Kartenausrichtung generell in Fortbewegungsrichtung gewählt. Insbesondere für die Darstellung von Kartenbeschriftung, stellen diese Möglichkeiten eine Herausforderung dar. In der vorliegende Arbeit wird ein Konzept zur Gestaltung von Beschriftungen in interaktiven Karten, die stufenloses Zoomen, Verschieben und Rotieren des Kartenausschnitts ermöglichen, vorgestellt. Dabei wird insbesondere die Beschriftung von sogenannten ”Points of Interest” - also zu beschriftenden Punkten - thematisiert. Derartige Beschriftungen sind gewöhnlich horizontal ausgerichtet und überlappen sich somit tendenziell bei der Kartenrotation. Vor allem beim Zoomen der Karte sind verschiedene Konsistenzkriterien zu beachten - so soll beispielsweise eine Beschriftung während eines kontinuierlichen Zoomens nicht mehrfach hinzugefügt und wieder entfernt werden. Außerdem sollen Beschriftungen von wichtigeren Punkten länger sichtbar sein, als solche von weniger wichtigen Punkten. Bei der Beschriftung von Gebieten gilt, dass sich die Beschriftung im Gebiet befinden und die grobe Form des Gebiets adaptieren soll. Um letzteres zu erreichen, darf die Beschriftung entlang eines Kreisbogens gebogen sein. Rotation ist in diesem Szenario einfach - die Beschriftung muss lediglich in ihrer Ausrightung umgekehrt werden, sodass sie nicht auf dem Kopf steht. Beim Zoomen des Kartenausschnitts sollten Gebiete als Ganzes oder ihre Untergebiete beschriftet werden, abhängig von der Kartenskala der Gebietsbeschriftung. Für der Beschriftung von Punkten werden sogenannte ”Disk-Label” eingeführt. Bei diesen wird für jede Beschriftung ein kreisförmiger Bereich um den zu beschriftenden Punkt reserviert. Die Beschriftung des Punkts bleibt in beliebigen Ausrichtungen der Karte vollständig in diesem Bereich enthalten. Indem als Beschriftung in einer beliebigen Kartenskala eine überschneidungsfreie Untermenge der ”Disk-Label” gewählt wird, ist die lesbare Darstellung bei Rotation gewährleistet. Beim Herauszoomen aus dem Kartenausschnitt, werden die Beschriftungen bei konstanter Größe beibehalten. Entsprechend wachsen die zugehörigen Disks relativ zur Karte - entsprechend schrumpfen die Distanzen zwischen den Disks. Bei fortschreitendem Zoomen, kommt es zu Berührungen der Disks. Dabei muss eine der beteiligten Beschriftungen muss entfernt, um bei weiterem Zoomen die überschneidungsfreiheit zu erhalten. Wird der entsprechende Zoomprozess von ”unendlich 107weit hineingezoomt” zu ”unendlich weit herausgezoomt” betrachtet, ergibt sich eine sogenannte Eliminationssequenz der Beschriftungen. Diese kann für einen Datensatz im Voraus berechnet werden und ermöglicht dann eine einfache, effiziente Ableitung einer Kartenbeschriftung für ein gegebenes Darstellungszenario. Das Problem der Berechnung der Eliminationssequenzen kann verallgemeinert in einem d-dimensionalen Hyperraum betrachtet werden. Entsprechend der Disks in 2D, wachsen d-dimensionalen Hyperbälle. Eine Eiminationssequenz ist dabei nicht eindeutig - kollidieren Bälle der selben Wichtigkeit, ist die Entscheidung welcher der beiden Bälle eliminiert wird, essentiell für den weiteren Verlauf der Sequenz. Das Ziel ist die Berechnung einer optimalen Sequenz, in der die Summe aller Eliminationszeitpunkte maximiert wird. Es wird gezeit, dass die Berechnung einer solchen optimalen Sequenz N P − hart ist. Für ein vereinfachtes Szenario - in welchem die Sequenz eindeutig ist - wird ein effizientes Berechnungsverfahren vorgestellt und analysiert. Dieses Verfahren hängt stark von einer effizienten Methode zur Berechnung des nächsten Nachbarn sowie der Suche nach Punkten mit einer maximalen Distanz zu einem gegebenen Punkt ab. Je nach Szenario können diese Operationen effizienter oder weniger effizient gelöst werden. Für 2D und für höhere Dimmensionen werden zwei verschiedene theoretische Laufzeitschranken bewiesen. Für die praktische Beschriftung von digitalen Karten, werden Punkte auf einem virtuellen Globus betrachtet. Eine Berechnung der Sequenz für 13 Millionen Punkte ist auf einem herkömmlichen Computer in etwa 15 Minuten möglich. Das ursprüngliche, unvereinfachte Problem kann mittels eines Mixed-Integer Linearen Programms für wenige Punkte exakt gelöst werden. Allerdings nur mit erheblichem Rechen- und Speicheraufwand. Eine gute Approximation der optimalen Sequenz bieten Heuristiken. Mittels dieser kann der vorgestellte Algorithmus für das vereinfachte Szenario Lösungen für das unvereinfachte Problem berechnen. In der Güte liegen die Heuristiken bei 5% − 10% unter dem Optimum. Bei Berechnungszeiten von 15 − 20 Minuten auf einem herkömmlichen Computer. Eine Gebietsbeschriftung liegt vollständig innerhalb des Gebiets und ahmt die Form des Gebiets nach, indem sie entlang eines Kreisbogens plaziert ist. Für eine gute Beschriftung ist eine entsprechende Platzierung gesucht, welche die Größe der Beschriftung maximiert. Abhängig davon kann eine maximale und minimale Kartenskala berechnet werden, bei welcher die Beschriftung lesbar dargestellt werden kann. Entsprechend kann das Gebiet bei größeren Skalen in einer weiteren Verfeinerung dargestellt, oder bei kleineren Skalen durch eine Punkt-Beschriftung oder die Darstellung eines umfassenden Gebiets ersetzt werden. Für die Berechnung einer solchen guten Beschriftung wird in der vorliegenden Arbeit ein effizienter Algorithmus vorgestellt. Dieser basiert auf einem Algorithmus von 2001, von M. Barrault in [Mat01] publiziert. Durch verschiedene Optimierungen kann diese Berechnung auf Quasi-Echtzeit verbessert werden.