Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
- 2005 (8) (remove)
Document Type
- Report (4)
- Doctoral Thesis (2)
- Master's Thesis (2)
Has Fulltext
- yes (8)
Keywords
- Akquisition (1)
- Algorithmus (1)
- Audiodeskription (1)
- Automatische Klassifikation (1)
- Automatisches Beweisverfahren (1)
- Effizienter Algorithmus (1)
- Implementierung (1)
- Java (1)
- Knuth-Bendix completion (1)
- Knuth-Bendix-Vervollständigung (1)
Faculty / Organisational entity
Wireless LANs operating within unlicensed frequency bands require random access schemes such as CSMA/ CA, so that wireless networks from different administrative domains (for example wireless community networks) may co-exist without central coordination, even when they happen to operate on the same radio channel. Yet, it is evident that this Jack of coordination leads to an inevitable loss in efficiency due to contention on the MAC layer. The interesting question is, which efficiency may be gained by adding coordination to existing, unrelated wireless networks, for example by self-organization. In this paper, we present a methodology based on a mathematical programming formulation to determine the
parameters (assignment of stations to access points, signal strengths and channel assignment of both access points and stations) for a scenario of co-existing CSMA/ CA-based wireless networks, such that the contention between these networks is minimized. We demonstrate how it is possible to solve this discrete, non-linear optimization problem exactly for small
problems. For larger scenarios, we present a genetic algorithm specifically tuned for finding near-optimal solutions, and compare its results to theoretical lower bounds. Overall, we provide a benchmark on the minimum contention problem for coordination mechanisms in CSMA/CA-based wireless networks.
Das Handlungsreisendenproblem ist eines der bekanntesten NP-vollständigen kombinatorischen Optimierungsprobleme. Algorithmen mit unterschiedlichen Konzepten und Strategien wurden entwickelt, die sich in Lösungsqualität und Laufzeit unterscheiden. Ein vergleichsweise neuer Ansatz stellt jedoch das Kombinieren vorhandener Lösungen dar. Hier werden die Kantenmengen gegebener Handlungsreisendertouren als Ausgangsbasis für weitere Optimierungen verwendet. Erste Veröffentlichungen zu diesem Gebiet stellen bereits vielversprechende Ergebnisse vor, die nachfolgend vertieft evaluiert werden.
This document introduces the extension of Katja to support position structures and explains the subtleties of their application as well as the design decisions made and problems solved with respect to their implementation. The Katja system was first introduced by Jan Schäfer in the context of his project work and is based on the MAX system developed by Arnd Poetzsch-Heffter.
Automated theorem proving is a search problem and, by its undecidability, a very difficult one. The challenge in the development of a practically successful prover is the mapping of the extensively developed theory into a program that runs efficiently on a computer. Starting from a level-based system model for automated theorem provers, in this work we present different techniques that are important for the development of powerful equational theorem provers. The contributions can be divided into three areas: Architecture. We present a novel prover architecture that is based on a set-based compression scheme. With moderate additional computational costs we achieve a substantial reduction of the memory requirements. Further wins are architectural clarity, the easy provision of proof objects, and a new way to parallelize a prover which shows respectable speed-ups in practice. The compact representation paves the way to new applications of automated equational provers in the area of verification systems. Algorithms. To improve the speed of a prover we need efficient solutions for the most time-consuming sub-tasks. We demonstrate improvements of several orders of magnitude for two of the most widely used term orderings, LPO and KBO. Other important contributions are a novel generic unsatisfiability test for ordering constraints and, based on that, a sufficient ground reducibility criterion with an excellent cost-benefit ratio. Redundancy avoidance. The notion of redundancy is of central importance to justify simplifying inferences which are used to prune the search space. In our experience with unfailing completion, the usual notion of redundancy is not strong enough. In the presence of associativity and commutativity, the provers often get stuck enumerating equations that are permutations of each other. By extending and refining the proof ordering, many more equations can be shown redundant. Furthermore, our refinement of the unfailing completion approach allows us to use redundant equations for simplification without the need to consider them for generating inferences. We describe the efficient implementation of several redundancy criteria and experimentally investigate their influence on the proof search. The combination of these techniques results in a considerable improvement of the practical performance of a prover, which we demonstrate with extensive experiments for the automated theorem prover Waldmeister. The progress achieved allows the prover to solve problems that were previously out of reach. This considerably enhances the potential of the prover and opens up the way for new applications.
Ultraschall ist eines der am häufigsten genutzen, bildgebenden Verfahren in der Kardiologie. Dies ist durch die günstige Erzeugung, die Nicht-Invasivität und die Unschädlichkeit für die Patienten begründet. Nachteilig an den existierenden Geräten ist der Umstand, daß lediglich zwei-dimensionale Bilder generiert werden können. Zusätzlich können diese Bilder aufgrund anatomischer Gegebenheiten nicht aus einer wahlfreien Position akquiriert werden. Dies erschwert die Analyse der Daten und folglich die Diagnose. Mit dieser Arbeit wurden neue, algorithmische Aspekte des vier-dimensionalen, kardiologischen Ultraschalls ausgehend von der Akquisition der Rohdaten, deren Synchronisation und Rekonstruktion bis hin zur Visualisierung bearbeitet. In einem zusätzlichen Kapitel wurde eine neue Technik zur weiteren Aufwertung der Visualisierung, sowie zur visuellen Bearbeitung der Ultraschalldaten entwickelt. Durch die hier entwickelten Verfahren ist es möglich bestimmte Einschränkungen des kardiologischen Ultraschalls aufzuheben oder zumindest zu mildern. Hierunter zählen vor allem die Einschränkung auf zwei-dimensionale Schnittbilder, sowie die eingeschränkte Sichtwahl.
There is a well known relationship between alternating automata on finite words and symbolically represented nondeterministic automata on finite words. This relationship is of practical relevance because it allows to combine the advantages of alternating and symbolically represented nondeterministic automata on finite words. However, for infinite words the situation is unclear. Therefore, this work investigates the relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Thereby, we identify classes of alternating omega-automata that are as expressive as safety, liveness and deterministic prefix automata, respectively. Moreover, some very simple symbolic nondeterminisation procedures are developed for the classes corresponding to safety and liveness properties.
Music Information Retrieval (MIR) is an interdisciplinary research area that has the goal to improve the way music is accessible through information systems. One important part of MIR is the research for algorithms to extract meaningful information (called feature data) from music audio signals. Feature data can for example be used for content based genre classification of music pieces. This masters thesis contributes in three ways to the current state of the art: • First, an overview of many of the features that are being used in MIR applications is given. These methods – called “descriptors” or “features” in this thesis – are discussed in depth, giving a literature review and for most of them illustrations. • Second, a large part of the described features are implemented in a uniform framework, called T-Toolbox which is programmed in the Matlab environment. It also allows to do classification experiments and descriptor visualisation. For classification, an interface to the machine-learning environment WEKA is provided. • Third, preliminary evaluations are done investigating how well these methods are suited for automatically classifying music according to categorizations such as genre, mood, and perceived complexity. This evaluation is done using the descriptors implemented in the T-Toolbox, and several state-of-the-art machine learning algorithms. It turns out that – in the experimental setup of this thesis – the treated descriptors are not capable to reliably discriminate between the classes of most examined categorizations; but there is an indication that these results could be improved by developing more elaborate techniques.
Das Ziel dieser Arbeit ist es, ein Framework und einen funktionsfähigen Prototypen für eine Middleware zu entwickeln, die es ermöglicht, Berechnungen verteilt in einem Peer-to-Peer-Netz auszuführen. Dabei sollen verschiedene Arten der Berechnung unterstützt werden. Eine Art der Berechnung sind Aufträge, die massiv parallel berechnet werden können, d.h. solche, die in unabhängige Teilaufträge zerlegt werden können und ohne gegenseitige Kommunikation auskommen. Diese Aufträge können entweder so parametrisiert sein, dass jeder Teilauftrag einen anderen Satz Parameter erhält (z.B. Fraktalberechnung), oder zufallsbasiert, so dass jeder Teilauftrag mit den gleichen Ausgangswerten berechnet wird und unterschiedliche Ergebnisse resultieren. Eine andere Art der Berechnung setzt voraus, dass Knoten, die am gleichen Auftrag arbeiten, auch miteinander kooperieren und durch Nachrichten beispielsweise Teillösungen austauschen (z.B. verteilte evolutionäre Algorithmen). Alle Knoten in diesem Netz sollen gleichberechtigt sein, d.h. jedem Knoten soll es möglich sein, eigene Anwendungen und Aufgaben im Netz zu verteilen. Den verteilten Anwendungen soll zudem die Möglichkeit gegeben werden, mit anderen Knoten, die an der gleichen Aufgabe arbeiten, kommunizieren zu können. Alle benötigten Informationen zur Berechnung eines Auftrags (d.h. Parameter, ausführbarer Code der Anwendung, Anzahl der zu berechnenden Fälle) sollen den rechnenden Knoten durch Middlewarefunktionen zur Verfügung gestellt werden, ebenso soll der Rücktransport der Ergebnisse zum Initiator durch die Middleware erfolgen. Der Nutzer soll also an seinem Arbeitsplatz seine verteilte Anwendung starten können und die Ergebnisse schließlich wieder auf seinem Rechner vorfinden. Die Implementierung soll möglichst modular angelegt sein und nicht auf ein konkretes P2P-Protokoll beschränkt sein, sondern einen leichten Austausch bzw. eine nutzergesteuerte Auswahl von verschiedenen Protokollen ermöglichen. Im Rahmen dieses Prototypen soll ein epidemisches P2P-Protokoll realisiert werden.