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 Emulation von Rechnernetzen zur Leistungsanalyse von verteilten Anwendungen und Netzprotokollen(2005) Herrscher, Daniel J.; Rothermel, Kurt (Prof. Dr. rer. nat. Dr. h. c)Um die Leistung von verteilten Anwendungen und Netzprotokollen in Abhängigkeit von den Eigenschaften der verwendeten Rechnernetze zu analysieren, wird eine Testumgebung benötigt, die Netzeigenschaften zuverlässig nachbilden ("emulieren") kann. Eine solche Testumgebung wird Emulationssystem genannt. Bisher existierende Emulationssysteme sind aufgrund ihrer Architektur entweder nur für sehr kleine Szenarien geeignet, oder sie können nur unabhängige Netzverbindungen nachbilden, und schließen damit alle Netztechnologien mit gemeinsamen Medien aus. In dieser Arbeit werden zunächst verschiedene Architekturvarianten für die Realisierung eines Emulationssystems vorgestellt und bewertet. Für die Variante mit zentraler Steuerung und verteilten Emulationswerkzeugen wird dann detailliert die Funktionalität eines Emulationssystems mit seinen wesentlichen Komponenten beschrieben. Das in dieser Arbeit entwickelte Emulationsverfahren greift auf der logischen Ebene der Sicherungsschicht in den Kommunikationsstapel ein. Auf dieser Ebene werden die beiden Basiseffekte Rahmenverlust und Verzögerung durch verteilte Emulationswerkzeuge nachgebildet. Alle anderen Netzeigenschaften können auf diese Basiseffekte zurückgeführt werden. Um Netztechnologien mit gemeinsamen Medien durch verteilte Werkzeuge nachbilden zu können, wird zusätzlich das Konzept des virtuellen Trägersignals eingeführt. Hierbei werden die Eigenschaften eines Rundsendemediums nachgebildet, indem kooperative Emulationswerkzeuge Rundsendungen zur Signalisierung eines Trägersignals benutzen. Somit kann jedeWerkzeuginstanz lokal ein aktuelles Modell des emulierten gemeinsamen Mediums halten. Auf dieser Basis kann auch das Verhalten von Medienzugriffsprotokollen nachgebildet werden. Die Arbeit deckt auch die wesentlichen Realisierungsaspekte eines Emulationssytems ab. Mit ausführlichen Messungen wird gezeigt, dass das entwickelte System für die Nachbildung von Netzszenarien sehr gut geeignet ist, selbst wenn die nachzubildenden Parameter sich dynamisch ändern. Die entwickelten Werkzeuge sind in der Lage, Netzeigenschaften in einem weiten Parameterbereich realistisch nachzubilden. Mit diesem System steht nun eine ideale Testumgebung für Leistungsmessungen von verteilten Anwendungen und Netzprotokollen in Abhängigkeit von Netzeigenschaften zur Verfügung.Item Open Access The design and implementation of a presentation system for interactive 3D graphics applications(2005) Stegmaier, Simon; Klein, Thomas; Strengert, Magnus; Ertl, ThomasWe present the design and implementation of a stand-alone system for presenting interactive 3D graphics applications and arbitrary multimedia contents to a public audience. The description includes technical details regarding the construction of a sturdy case to accommodate touchscreen, PC, video projector, and sound equipment, and details involved in the design of the presentation software. The presented system was evaluated during a week-long exhibition with several hundreds of users.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 Laws for rewriting queries containing division operators(2005) Rantzau, Ralf; Mangold, ChristophRelational division, also known as small divide, is a derived operator of the relational algebra that realizes a many-to-one set containment test, where a set is represented as a group of tuples: Small divide discovers which sets in a dividend relation contain all elements of the set stored in a divisor relation. The great divide operator extends small divide by realizing many-to-many set containment tests. It is also similar to the set containment join operator for schemas that are not in first normal form. Neither small nor great divide has been implemented in commercial relational database systems although the operators solve important problems and many efficient algorithms for them exist. We present algebraic laws that allow rewriting expressions containing small or great divide, illustrate their importance for query optimization, and discuss the use of great divide for frequent itemset discovery, an important data mining primitive. A recent theoretic result shows that small divide must be implemented by special purpose algorithms and not be simulated by pure relational algebra expressions to achieve efficiency. Consequently, an efficient implementation requires that the optimizer treats small divide as a first-class operator and possesses powerful algebraic laws for query rewriting.Item Open Access Standardisierte Auszeichnungssprachen der Computergraphik für interaktive Systeme(2005) Rotard, Martin; Ertl, Thomas (Prof. Dr.)Computergraphik wird in vielen Bereichen der anwendungsorientierten Informatik, von der optischen Gestaltung graphischer Benutzungsoberflächen bis zur Visualisierung wissenschaftlicher Zusammenhänge eingesetzt. Auszeichnungssprachen zur Beschreibung graphischer Information erweitern diese Einsatzmöglichkeiten um die Animation und die Interaktion mit den Inhalten. In dieser Arbeit werden neue Verfahren und Strategien entwickelt, die den Einsatz von standardisierten Auszeichnungssprachen der Computergraphik in den Bereichen Benutzungsoberflächen und Lehrmaterialien ermöglichen. Dabei liegt ein Schwerpunkt auf der Zugänglichkeit von graphischen Inhalten für blinde Menschen, insbesondere durch interaktive Exploration von taktilen Darstellungen. Diese Arbeit stellt Methoden für die Beschreibung von skalierbaren Interaktionselementen mit Auszeichnungssprachen vor, die an verschiedenste Anzeigegeräte angepasst werden können. Darauf aufbauend entstanden neue Konzepte für zoombare Benutzungsoberflächen zur variablen Größendarstellung von Interaktionselementen und deren Inhalten. Erstmals werden auch Methoden vorgestellt, um die Darstellung von Benutzungsoberflächen, die mit Auszeichnungssprachen beschrieben werden, auf andere Rechner zu übertragen. Der Einsatz von Graphiken, die auf Auszeichnungssprachen basieren, bietet bei deren Erstellung, Handhabung und Anwendung erhebliche Vorteile gegenüber herkömmlicher Rastergraphik. Diese Arbeit stellt neue Verfahren vor, um die Formatierungen von Graphiken in Lehrmodulen anzupassen. Entwickelt werden unter anderem Konzepte für die Generierung von Lehrmodulen, die eine flexible Wiederverwendung in verschiedenen Lernszenarien ermöglichen. Für blinde Menschen bilden textuelle Inhalte die Hauptinformationsquelle bei ihrer Arbeit mit Computersystemen. Die ganzheitliche Darstellung von textuellen und graphischen Inhalten ist für viele Anwendungen jedoch unabdingbar. Mit Graphik, die auf Auszeichnungssprachen basiert, können erstmals Verfahren für die taktile Repräsentation präsentiert werden, die eine ganzheitliche Erschließung der graphischen Inhalte ermöglichen. Dazu werden Methoden vorgestellt, die blinden Menschen den Zugang zu mathematischen Ausdrücken, zu 2D- und zu 3D-Graphiken gestatten. Dies wird an einem taktilen Web-Browser demonstriert, der den Zugang zu diesen unterschiedlichen Graphikarten integriert.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 Ionenunterstützte Antimon-Dotierung für die Silizium-Molekularstrahlepitaxie von Bauelementstrukturen(2005) Eifler, Georg; Kasper, Erich (Prof. Dr. phil.)Die Molekularstrahlepitaxie (MBE) ist eine geeignete Methode zur Herstellung von aktuellen Höchstfrequenz-Bauelementstrukturen, wie dem Silizium-Germanium-Heterobipolartransistor (SiGe-HBT) mit einer ultradünnen (< 20 nm), hochdotierten Basis. Die MBE ermöglicht eine starke Reduzierung der Wachstumstemperatur, um Dotier- und Heterostrukturprofile mit Nanometer-Abmessungen zu erzeugen. In diesem Niedrigtemperatur-Bereich mit vernachlässigbarer Volumendiffusion zeigt sich, dass auch die Entmischung der Materialien an der wachsenden Oberfläche durch Segregation zu einer Verschmierung der Profile führt. Die Segregation kann durch eine passende Strategie verhindert werden, wenn das Ausmaß der Segregation in Abhängigkeit der beeinflussenden Parameter bekannt ist. In dieser Arbeit wird eine Wachstumsstrategie für einen npn-SiGe-HBT vorgestellt. Die Strategie und ihre Umsetzung werden anhand der Profile und elektrischen Ergebnisse diskutiert. Der Schwerpunkt der Untersuchungen wurde auf die exakte Verwirklichung des n-Dotierprofils mit Antimon (Sb) gelegt. Antimon neigt sehr stark zur Segregation, bietet jedoch gegenüber anderen Elementen der V. Hauptgruppe große Vorteile bei der Verdampfung im Ultrahoch-Vakuum (UHV). Als Maß für die Segregation wurde die Segregationsweite D in Abhängigkeit der Wachstumsparameter Temperatur T, Wachstumsrate R und Sb-Oberflächenkonzentration nS bestimmt. Weiterhin wurde die Möglichkeit aufgezeigt, die Segregation durch den Einfluss niederenergetischer Ionen zu unterdrücken. Bei dieser Dotierung mit Sekundärionen (DSI) werden Sb-Oberflächenatome durch im Substratpotenzial beschleunigte Ionen einige Atomlagen tief in den Kristall gestoßen und durch Umordnung der Atome eingebaut. Der Silizium-Elektronenstrahlverdampfer (Si-ESV) ist eine geeignete Ionenquelle, die ohne zusätzlichen Aufwand für das ionenunterstützte MBE-Wachstum genutzt werden kann. Die Generation und Ausbreitung von Ionen sowie deren Einfluss auf die Dotierung wurde anhand des Stroms am Substratkontakt und einer im Rahmen einer wissenschaftlichen Zusammenarbeit mit der Akademie der Wissenschaften in Tashkent/Usbekistan entwickelten Ionensonde untersucht. Des Weiteren wurden zur Untersuchung der Segregation und der ionenbedingten Dotierung MBE-Schichten durch das Wachstum mit Vorbelegung unter Variation der entscheidenden Wachstumsparameter hergestellt. Die Ergebnisse der Vierspitzenmessung, der elektrochemischen Kapazitäts-Spannungsmessung (eCV) und der Sekundärionen-Massen-spektroskopie (SIMS) zeigen die Segregationsweite D in Abhängigkeit der beeinflussenden Parameter. Mit den Ergebnissen der Segregation und des ionenbedingten Einbaus können exakte Sb-Dotierprofile mit scharfen Übergängen für Bauelementstrukturen verwirklicht werden. Beim Wachstums mit Vorbelegung wird die Dotierung über die Segregationsweite, bzw. durch deren beeinflussende Parameter gesteuert. Am besten eignen sich dazu die Variation der Wachstumstemperatur oder der Ionendichte über die Substratspannung. Darauf aufbauend wurde ein HBT-Konzept mit einem niedrigdotierten 300 nm- Kollektor, hochdotierter 25 nm-Basis mit 3 nm-Zwischenschichten und einem dreiteiligen Emitter, bestehend aus "low doped"-, "high doped"-Emitter und Emitterkontakt umgesetzt. Als Vorstufe wurden Emitter-Basis-(EB-)Dioden und Basis-Kollektor-(BC-)Dioden hergestellt und deren SIMS-Profile und Diodenkennlinien untersucht. In den Dotierprofilen zeigen sich Abweichungen von den Segregationsergebnissen, wenn sich die Oberflächenkonzentrationen von Sb, Bor und Ge gegenseitig beeinflussen und sogenannte surfactant-Effekte zeigen, die in dieser Arbeit jedoch nicht weiter verfolgt werden. Aus den Ergebnissen der beiden Einzeldioden wurde eine HBT-Wachstumsstrategie entwickelt. Die wesentlichen Merkmale dieser Strategie sind der DSI-Kollektor zu Wachstumsbeginn und die Dotierung des "low doped"-Emitters. Beim Wachstum des Kollektors und der Basis wird nur ein geringer Teil der ursprünglichen Sb-Vorbelegung verbraucht, so dass diese zu Beginn des "low doped"-Emitters noch fast vollständig vorhanden ist. Mit dieser Vorbelegung kann die Dotierung des "low doped"-Emitters über die Wachstumstemperatur gesteuert werden. Im Dotierprofil des "high doped" Emitters und der Emitterkontaktschicht spiegelt sich die Abhängigkeit der Segregationsweite von der Sb-Oberflächenkonzentration wider. Mit den hergestellten Strukturen wurde der Nachweis eines funktionierenden npn-SiGe-HBTs erbracht, dessen gesamtes Dotierprofil in einem einzigen Prozessschritt durch MBE-Wachstum erzeugt wurde. Dabei wurden mit technologisch gut beherrschbaren Werten des Germaniumgehalts (16 %) und totaler Basisweite von 31 nm Verstärkungen b0 > 60 erreicht.Item Open Access Models for transient simulations of decentral power generation : implementation and verification in PowerFactory(2005) Braun, MartinAs part of the Institut für Solare Energieversorgungstechnik (ISET) e.V. in Kassel, the Design Center for Modular Supply Technology (DeMoTec) has the facilities for testing a variety of low-voltage power grid configurations. These configurations consist of decentralized power generation components in the kilowatt range. Transient simulations of components and grid configurations with MATLAB/Simulink, ATP-EMTP and SIMPLORER support research activities in this field. The aim of this work is to add a fourth tool - PowerFactory - which offers additional features for this application. All four simulation tools have their own specific characteristics which make them most suitable for particular applications. This work investigates the features of PowerFactory developed by DIgSILENT. The investigation uses components for grid configurations which are available in DeMoTec in order to verify the results of the simulations by measurements. The island grids which are investigated comprise three components: a bi-directional battery inverter which is able to form a grid, an asynchronous generator which simulates the feed-in of wind power, and a load which represents consumers and their consumption behaviour. In order to allow these components to be used in PowerFactory, this work presents the following three parts for the implementation of the components' models: 1) PowerFactory does not comprise a generic model for a battery inverter. However, single phase models in MATLAB/Simulink and ATP-EMTP are available which deliver details for the development of a PowerFactory model. For the implementation, the available models are enhanced to a three phase model and adjusted to the simulation environment of PowerFactory. 2) PowerFactory comprises a model for asynchronous generators. This generic model is adjusted to the considered asynchronous generator in DeMoTec. The electrical parameters of the analysed asynchronous generator are measured for this adjustment process and an optimisation process is performed to determine best fitting parameters. 3) A generic model for loads is available in PowerFactory. It is adjusted to correspond to the loads used in DeMoTec. The models implemented in PowerFactory form different configurations of island grids. Within these island grids, PowerFactory simulates characteristic load changes. The selected components enable measurements of the same load changes in the same grid configurations in DeMoTec. A comparison of the measured and simulated data shows a good congruence with few deviations. This thesis uses the power system analysis tool PowerFactory from DIgSILENT for transient simulations of decentralised power generation components in low-voltage grids which operate with a variable frequency and a variable voltage. Moreover, this thesis verifies the simulation results and illustrates their quality by comparing measured data at DeMoTec with simulated data using PowerFactory. Finally, one of the advantages of this simulation tool is presented by simulating a large grid configuration which is not available in the limited laboratory environment of DeMoTec.