Starfree regular languages can be build up from alphabet letters by using only Boolean operations and concatenation. The complexity of these languages can be measured with the so-called dot-depth. This measure leads to concatenation hierarchies like the dot-depth hierarchy (DDH) and the closely related Straubing-Thérien hierarchy (STH). The question whether the single levels of these hierarchies are decidable is still open and is known as the dot-depth problem. In this thesis we prove/reprove the decidability of some lower levels of both hierarchies. More precisely, we characterize these levels in terms of patterns in finite automata (subgraphs in the transition graph) that are not allowed. Therefore, such characterizations are called forbidden-pattern characterizations. The main results of the thesis are as follows: forbidden-pattern characterization for level 3/2 of the DDH (this implies the decidability of this level) decidability of the Boolean hierarchy over level 1/2 of the DDH definition of decidable hierarchies having close relations to the DDH and STH Moreover, we prove/reprove the decidability of the levels 1/2 and 3/2 of both hierarchies in terms of forbidden-pattern characterizations. We show the decidability of the Boolean hierarchies over level 1/2 of the DDH and over level 1/2 of the STH. A technique which uses word extensions plays the central role in the proofs of these results. With this technique it is possible to treat the levels 1/2 and 3/2 of both hierarchies in a uniform way. Furthermore, it can be used to prove the decidability of the mentioned Boolean hierarchies. Among other things we provide a combinatorial tool that allows to partition words of arbitrary length into factors of bounded length such that every second factor u leads to a loop with label u in a given finite automaton. / Sternfreie reguläre Sprachen können aus Buchstaben unter Verwendung Boolescher Operationen und Konkatenation aufgebaut werden. Die Komplexität solcher Sprachen lässt sich durch die sogenannte "Dot-Depth" messen. Dieses Maß führt zu Konkatenationshierarchien wie der Dot-Depth-Hierachie (DDH) und der Straubing-Thérien-Hierarchie (STH). Die Frage nach der Entscheidbarkeit der einzelnen Stufen dieser Hierarchien ist als (immer noch offenes) Dot-Depth-Problem bekannt. In dieser Arbeit beweisen wir die Entscheidbarkeit einiger unterer Stufen beider Hierarchien. Genauer gesagt charakterisieren wir diese Stufen durch das Verbot von bestimmten Mustern in endlichen Automaten. Solche Charakterisierungen werden Verbotsmustercharakterisierungen genannt. Die Hauptresultate der Arbeit lassen sich wie folgt zusammenfassen: Verbotsmustercharakterisierung der Stufe 3/2 der DDH (dies hat die Entscheidbarkeit dieser Stufe zur Folge) Entscheidbarkeit der Booleschen Hierarchie über der Stufe 1/2 der DDH Definition von entscheidbaren Hierarchien mit engen Verbindungen zur DDH und STH Darüber hinaus beweisen wir die Entscheidbarkeit der Stufen 1/2 und 3/2 beider Hierarchien (wieder mittels Verbotsmustercharakterisierungen) und die der Booleschen Hierarchien über den Stufen 1/2 der DDH bzw. STH. Dabei stützen sich die Beweise größtenteils auf eine Technik, die von Eigenschaften bestimmter Worterweiterungen Gebrauch macht. Diese Technik erlaubt eine einheitliche Vorgehensweise bei der Untersuchung der Stufen 1/2 und 3/2 beider Hierarchien. Außerdem wird sie in den Beweisen der Entscheidbarkeit der genannten Booleschen Hierarchien verwendet. Unter anderem wird ein kombinatorisches Hilfsmittel zur Verfügung gestellt, das es erlaubt, Wörter beliebiger Länge in Faktoren beschränkter Länge zu zerlegen, so dass jeder zweite Faktor u zu einer u-Schleife in einem gegebenen endlichen Automaten führt.

The classic theorems of Büchi and Kleene state the expressive equivalence of finite automata to monadic second order logic and regular expressions, respectively. These fundamental results enjoy applications in nearly every field of theoretical computer science. Around the same time as Büchi and Kleene, Rabin investigated probabilistic finite automata. This equally well established model has applications ranging from natural language processing to probabilistic model checking. Here, we give probabilistic extensions Büchi\\\'s theorem and Kleene\\\'s theorem to the probabilistic setting. We obtain a probabilistic MSO logic by adding an expected second order quantifier. In the scope of this quantifier, membership is determined by a Bernoulli process. This approach turns out to be universal and is applicable for finite and infinite words as well as for finite trees. In order to prove the expressive equivalence of this probabilistic MSO logic to probabilistic automata, we show a Nivat-theorem, which decomposes a recognisable function into a regular language, homomorphisms, and a probability measure. For regular expressions, we build upon existing work to obtain probabilistic regular expressions on finite and infinite words. We show the expressive equivalence between these expressions and probabilistic Muller-automata. To handle Muller-acceptance conditions, we give a new construction from probabilistic regular expressions to Muller-automata. Concerning finite trees, we define probabilistic regular tree expressions using a new iteration operator, called infinity-iteration. Again, we show that these expressions are expressively equivalent to probabilistic tree automata. On a second track of our research we investigate Constraint LTL over multidimensional data words with data values from the infinite tree. Such LTL formulas are evaluated over infinite words, where every position possesses several data values from the infinite tree. Within Constraint LTL on can compare these values from different positions. We show that the model checking problem for this logic is PSPACE-complete via investigating the emptiness problem of Constraint Büchi automata.

In dieser Arbeit wird ein Verfahren für robustes Parsing von uneingeschränktem natürlichsprachlichen Text mit gewichteten Transduktoren erarbeitet. Es werden zwei linguistische Theorien, das Chunking und das syntaktische Tagging, vorgestellt, die sich besonders für die praktische Anwendung mit Finite-State Maschinen eignen. Über die formalen Grundlagen, die es möglich machen, Finite-State Maschinen zu modellieren, werden existierende Ansätze vorgestellt, die diese linguistischen Theorien mit Finite-State Maschinen realisieren. <br>Jedoch sind diese Ansätze in vieler Hinsicht problematisch. Es wird gezeigt, dass sich Probleme lösen lassen, indem Disambiguierungsstrategien durch Constraints realisiert werden, die als Gewicht bzw. Semiring vorliegen. Durch die Bestimmung des besten Pfades ist dann eine Disambiguierung möglich. Das Verfahren bewegt sich zwischen einem Low- und High-Level Parsing und behandelt flache Dependenzstrukturen. Für die Analyse wird eine rudimentäre Grammatik für das Deutsche entwickelt. Durch eine Implementierung wird letztlich der Ansatz getestet.

Regular path queries (RPQs) are a fundamental part of recent graph query languages like SPARQL and PGQL. They allow the definition of recursive path structures through regular expressions in a declarative pattern matching environment. We study the use of the K2-tree graph compression technique to materialize RPQ results with low memory consumption for indexing. Compact index representations enable the efficient storage of multiple indexes for varying RPQs.

Regular Path Queries (RPQs) are at the core of many recent declarative graph pattern matching languages. They leverage the compactness and expressiveness of regular expressions for matching recursive path structures. Unfortunately, most prior works on RPQs only consider breadth-first search as traversal strategy, neglecting other possible graph traversals like depth-first search or a combination of both. Within this paper, we conduct an analysis of graph traversals for RPQs by introducing a generalized graph traversal frame-work subsuming breadth-first search and depth-first search as extreme cases and thus opening up a new design space for graph traversals algorithms. We outline the underlying principles as well as provide comprehensive experimental evaluation using implementations which yield beneficial results regarding evaluation time and peak memory consumption.

Am Beispiel verschiedener Strömungstypen wird die Stabilität von Strömungen unter Einfluß eines Temperaturfeldes untersucht. Eine reguläre Störungs- rechnung wird durchgeführt, um die Effekte temperatur- abhängiger Stoffwerte systematisch und allgemein- gültig erfassen zu können. Die Ergebnisse werden in Form asymptotischer Reihen für die kritischen Kenn- zahlen der jeweiligen Probleme angegeben. Sowohl die Orr-Sommerfeld-Gleichungen als auch die PSE-Gleichungen, jeweils mit variablen Stoffwerten, kommen bei der Untersuchung von Grenzschicht- strömungen zum Einsatz. Von besonderem Interesse sind hier die Unterschiede in den Lösungen beider mathematischer Modelle bezüglich der Effekte variabler Stoffwerte. Es zeigt sich, dass die Differenzen in den Lösungen beider Theorien für den Fall konstanter und für den Fall variabler Stoffwerte gleich groß sind. Für die Grenzschichtströmung bei natürlicher Kon- vektion an einer beheizten vertikalen Wand werden die vollständigen PSE-Gleichungen gelöst. Hier zeigen sich starke Abweichungen zur lokalen paral- lelen Theorie (Orr--Sommerfeld--Gleichungen).

No description available.

The classic theorems of Büchi and Kleene state the expressive equivalence of finite automata to monadic second order logic and regular expressions, respectively. These fundamental results enjoy applications in nearly every field of theoretical computer science. Around the same time as Büchi and Kleene, Rabin investigated probabilistic finite automata. This equally well established model has applications ranging from natural language processing to probabilistic model checking. Here, we give probabilistic extensions Büchi\\\''s theorem and Kleene\\\''s theorem to the probabilistic setting. We obtain a probabilistic MSO logic by adding an expected second order quantifier. In the scope of this quantifier, membership is determined by a Bernoulli process. This approach turns out to be universal and is applicable for finite and infinite words as well as for finite trees. In order to prove the expressive equivalence of this probabilistic MSO logic to probabilistic automata, we show a Nivat-theorem, which decomposes a recognisable function into a regular language, homomorphisms, and a probability measure. For regular expressions, we build upon existing work to obtain probabilistic regular expressions on finite and infinite words. We show the expressive equivalence between these expressions and probabilistic Muller-automata. To handle Muller-acceptance conditions, we give a new construction from probabilistic regular expressions to Muller-automata. Concerning finite trees, we define probabilistic regular tree expressions using a new iteration operator, called infinity-iteration. Again, we show that these expressions are expressively equivalent to probabilistic tree automata. On a second track of our research we investigate Constraint LTL over multidimensional data words with data values from the infinite tree. Such LTL formulas are evaluated over infinite words, where every position possesses several data values from the infinite tree. Within Constraint LTL on can compare these values from different positions. We show that the model checking problem for this logic is PSPACE-complete via investigating the emptiness problem of Constraint Büchi automata.

Mit der steigenden Nachfrage nach Innovationen spielt Software in verschiedenenWirtschaftsbereichen eine wichtige Rolle, wie z.B. in der Automobilindustrie, bei intelligenten Systemen als auch bei Kommunikationssystemen. Daher ist die Qualität für die Softwareentwicklung von großer Bedeutung. Allerdings ändern sich die probabilistische Modelle (die Qualitätsbewertungsmodelle) angesichts der dynamischen Natur moderner Softwaresysteme. Dies führt dazu, dass ihre Übergangswahrscheinlichkeiten im Laufe der Zeit schwanken, welches zu erheblichen Problemen führt. Dahingehend werden probabilistische Modelle im Hinblick auf ihre Laufzeit kontinuierlich aktualisiert. Eine fortdauernde Neubewertung komplexer Wahrscheinlichkeitsmodelle ist jedoch teuer. In letzter Zeit haben sich inkrementelle Ansätze als vielversprechend für die Verifikation von adaptiven Systemen erwiesen. Trotzdem wurden bei der Bewertung struktureller Änderungen im Modell noch keine wesentlichen Verbesserungen erzielt. Wahrscheinlichkeitssysteme werden als Automaten modelliert, wie bei Markov-Modellen. Solche Modelle können in Matrixform dargestellt werden, um die Gleichungen basierend auf Zuständen und Übergangswahrscheinlichkeiten zu lösen. Laufzeitmodelle wie Matrizen sind nicht signifikant, um die Auswirkungen von Modellveränderungen erkennen zu können. In dieser Arbeit wird ein Framework unter Verwendung stochastischer Bäume mit regulären Ausdrücken entwickelt, welches modular aufgebaut ist und eine aktionshaltige sowie probabilistische Logik im Kontext der Modellprüfung aufweist. Ein solches modulares Framework ermöglicht dem Menschen die Entwicklung der Änderungsoperationen für die inkrementelle Berechnung lokaler Änderungen, die im Modell auftreten können. Darüber hinaus werden probabilistische Änderungsmuster beschrieben, um eine effiziente inkrementelle Verifizierung, unter Verwendung von Bäumen mit regulären Ausdrücken, anwenden zu können. Durch die Bewertung der Ergebnisse wird der Vorgang abgeschlossen. / Software plays an innovative role in many different domains, such as car industry, autonomous and smart systems, and communication. Hence, the quality of the software is of utmost importance and needs to be properly addressed during software evolution. Several approaches have been developed to evaluate systems’ quality attributes, such as reliability, safety, and performance of software. Due to the dynamic nature of modern software systems, probabilistic models representing the quality of the software and their transition probabilities change over time and fluctuate, leading to a significant problem that needs to be solved to obtain correct evaluation results of quantitative properties. Probabilistic models need to be continually updated at run-time to solve this issue. However, continuous re-evaluation of complex probabilistic models is expensive. Recently, incremental approaches have been found to be promising for the verification of evolving and self-adaptive systems. Nevertheless, substantial improvements have not yet been achieved for evaluating structural changes in the model. Probabilistic systems are usually represented in a matrix form to solve the equations based on states and transition probabilities. On the other side, evolutionary changes can create various effects on theese models and force them to re-verify the whole system. Run-time models, such as matrices or graph representations, lack the expressiveness to identify the change effect on the model. In this thesis, we develop a framework using stochastic regular expression trees, which are modular, with action-based probabilistic logic in the model checking context. Such a modular framework enables us to develop change operations for the incremental computation of local changes that can occur in the model. Furthermore, we describe probabilistic change patterns to apply efficient incremental quantitative verification using stochastic regular expression trees and evaluate our results.

Bacterial cell wall proteins (S-layer) are - due to both the capability to self-assemble into two-dimensional crystals and their distinct chemical and structural properties - suitable for the deposition of metallic particles at their surface . The cluster growth is subject of this thesis. The binding of metal complexes to S-layers of Bacillus sphaericus and Sporosarcina ureae and their subsequent reduction leads to the formation of regularly arranged platinum or palladium cluster arrays on the biomolecular template. A heterogeneous nucleation mechanism is proposed for this process consisting of the binding of metal complexes and their subsequent reduction. The kinetics of the process and the binding of the complexes to the protein are characterized by UV/VIS spectroscopy. This thesis focuses on structural investigations by means of transmission electron microscopy, electron holography, scanning force microscopy, image analysis, and image processing. Preferred cluster-deposition sites are determined by correlation averaging. A more precise determination and quantification is obtained by Multivariate Statistical Analysis. Furthermore a method for the electron beam induced formation of highly-ordered metallic cluster arrays in the transmission electron microscope and a fast screening method for surface layers of Gram-positive bacteria are presented. / Bakterielle Zellhüllenproteine (S-Layer) eignen sich durch ihre Fähigkeit zur Selbstassemblierung zu zweidimensionalen Kristallen und durch ihre besonderen chemischen und strukturellen Eigenschaften zur Abscheidung regelmäßiger metallischer Partikel auf ihrer Oberfläche. In dieser Arbeit wird das Clusterwachstum auf S-Layern untersucht. Die Anbindung von Metallkomplexen an S-Layer von Bacillus sphaericus und Sporosarcina ureae und deren Reduktion führt zur Abscheidung periodisch angeordneter metallischer Platin- bzw. Palladiumcluster auf dem Biotemplat. Für diese Clusterbildung wird ein heterogener Keimbildungsmechanismus vorgeschlagen, bestehend aus Komplexanbindung und Reduktion. Die Bestimmung der Prozeßkinetik und die Charakterisierung der Anbindung der Komplexe an das Protein erfolgt mittels UV/VIS-Spektroskopie. Den Schwerpunkt dieser Arbeit bilden strukturelle Untersuchungen mit Hilfe der Transmissionselektronenmikroskopie, der Elektronenholographie, der Rasterkraftmikroskopie und der Bildanalyse und Bildverarbeitung. Durch Korrelationsmittelung werden Strukturinformationen gewonnen, die eine Bestimmung der lateral bevorzugten Clusterpositionen ermöglichen. Für die auf S-Layern erzeugten Clusterarrays wird die Belegung der einzelnen Positionen mittels Multivariater Statistischer Analyse genauer quantifiziert. Außerdem werden eine Methode zur Erzeugung hochgeordneter metallischer Partikelarrays unter dem Einfluß des Elektronenstrahles im Transmissionselektronenmikroskop und eine Methode zum schnellen Test Gram-positiver Bakterienstämme auf die Existenz von S-Layern vorgestellt.