Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
Document Type
- Doctoral Thesis (235) (remove)
Has Fulltext
- yes (235)
Keywords
- Visualisierung (20)
- Visualization (8)
- Deep Learning (7)
- Computergraphik (5)
- Evaluation (4)
- Robotik (4)
- Artificial Intelligence (3)
- Bildverarbeitung (3)
- Geoinformationssystem (3)
- Machine Learning (3)
Faculty / Organisational entity
Termination of Rewriting
(1994)
More and more, term rewriting systems are applied in computer science aswell as in mathematics. They are based on directed equations which may be used as non-deterministic functional programs. Termination is a key property for computing with termrewriting systems.In this thesis, we deal with different classes of so-called simplification orderings which areable to prove the termination of term rewriting systems. Above all, we focus on the problemof applying these termination methods to examples occurring in practice. We introduce aformalism that allows clear representations of orderings. The power of classical simplifica-tion orderings - namely recursive path orderings, path and decomposition orderings, Knuth-Bendix orderings and polynomial orderings - is improved. Further, we restrict these orderingssuch that they are compatible with underlying AC-theories by extending well-known methodsas well as by developing new techniques. For automatically generating all these orderings,heuristic-based algorithms are given. A comparison of these orderings with respect to theirpowers and their time complexities concludes the theoretical part of this thesis. Finally, notonly a detailed statistical evaluation of examples but also a brief introduction into the designof a software tool representing the integration of the specified approaches is given.
Zur Planung und Steuerung von komplexen rechnerintegrierten Fertigungssystemen (CIM) ist die Abarbeitung vieler extrem aufwendiger Algorithmen notwendig. Aus dem Bereich der Fertigungssteuerung zählt die Generierung von Maschinenbelegungsplänen (scheduling) dazu. Zur Steigerung der Lösungsgeschwindigkeit bzw. zum Erreichen exakter Ergebnisse bietet sich der massive Einsatz von Rechenparallelität an. Mit Parallelrechnern ist durch die gleichzeitige Verwendung von vielen Prozessoren potentiell eine sehr große Leistungssteigerung zu erreichen. Dafür muß jedoch die vorhandene Parallelität effektiv genutzt werden. Die dazu erforderliche Verteilung der anstehenden Arbeit auf eine große Menge von Prozessoren heißt Lastverteilung und stellt den Kern dieser Arbeit dar. Als allgemeiner Algorithmus zur Lösung kombinatorischer Optimierungs-probleme wird das Branch-and-bound-Verfahren eingesetzt und auf fein-körnigen Parallelrechnerarchitekturen ausgeführt. Zur Lastverteilung werden folgende drei Ansätze verfolgt und untersucht: " Statische Lastverteilung: Es werden mehrere Methoden zur Initialisierung der Prozessoren, welche vor dem eigentlichen Optimierungsalgorithmus ausgeführt werden, analysiert. Es zeigt sich, daß sich die statische Last-verteilung überproportional stark auf die Laufzeit des nachfolgenden Branch-and-bound-Algorithmus auswirkt. Es ist daher wichtig, der bisher unterschätzten statischen Lastverteilung für die parallele Baumsuche mit realen Problemstellungen, besondere Aufmerksamkeit zu schenken. " Dynamische Lastverteilung: Es wird ein vereinfachtes, gut skalierbares Flüssigkeitsmodell als erste synchrone lokale Lastverteilung entwickelt, welche besonders für Parallelrechner mit kurzer Verzögerungszeit beim Aufbau von Kommunikationsverbindungen effizient ist. Die Methode wird mit dem bekannten, aus dem Asynchronen übertragenen, Mittelungs-Ansatz verglichen. Zum analytischen Vergleich wird als ein realistischeres Aufwandsmaß die Kommunikationsmenge statt der üblichen Anzahl von Kommunikationsschritte verwendet. Der in der Prozessoranzahl bisher benötigte quadratische Zeitaufwand wird durch das Flüssigkeitsmodell auf einen linearen Aufwand reduziert, wobei das Flüssigkeitsmodell auch bzgl. der konstanten Zeitfaktoren signifikant effizienter ist. " Implizite Lastverteilung: Zur Vermeidung von Wartezeiten der unbe-teiligten Prozessoren während der Lastverteilung wird der Lastverteilungs-prozeß mit dem Branch-and-bound-Prozeß verschmolzen. Das neuartige Konzept der k-Expansion unterstützt eine automatische Lastverteilung und approximiert eine globale Suchstrategie. Zur Validierung der Ergebnisse werden Simulationen und Experimente mit einem Satz von Benchmark-Problemen durchgeführt. Der zugrunde liegende SIMD-Rechner ist eine MasPar MP-1 mit 16.384 Prozessoren in einem 2- dimensionalen Torus. Als exemplarische, NP-harte Anwendungsdomäne werden statische, non-operationale Planungsprobleme betrachtet.
In dieser Dissertation wird das Konzept der Gröbnerbasen für endlich erzeugte Monoid-und Gruppenringe verallgemeinert. Dabei werden Reduktionsmethoden sowohl zurDarstellung der Monoid- beziehungsweise Gruppenelemente, als auch zur Beschreibungder Rechtsidealkongruenz in den entsprechenden Monoid- beziehungsweise Gruppenrin-gen benutzt. Da im allgemeinen Monoide und insbesondere Gruppen keine zulässigenOrdnungen mehr erlauben, treten bei der Definition einer geeigneten Reduktionsrela-tion wesentliche Probleme auf: Zum einen ist es schwierig, die Terminierung einer Re-duktionsrelation zu garantieren, zum anderen sind Reduktionsschritte nicht mehr mitMultiplikationen verträglich und daher beschreiben Reduktionen nicht mehr unbedingteine Rechtsidealkongruenz. In dieser Arbeit werden verschiedene Möglichkeiten Reduk-tionsrelationen zu definieren aufgezeigt und im Hinblick auf die beschriebenen Problemeuntersucht. Dabei wird das Konzept der Saturierung, d.h. eine Polynommenge so zu er-weitern, daß man die von ihr erzeugte Rechtsidealkongruenz durch Reduktion erfassenkann, benutzt, um Charakterisierungen von Gröbnerbasen bezüglich der verschiedenenReduktionen durch s-Polynome zu geben. Mithilfe dieser Konzepte ist es gelungenfür spezielle Klassen von Monoiden, wie z.B. endliche, kommutative oder freie, undverschiedene Klassen von Gruppen, wie z.B. endliche, freie, plain, kontext-freie odernilpotente, unter Ausnutzung struktureller Eigenschaften spezielle Reduktionsrelatio-nen zu definieren und terminierende Algorithmen zur Berechnung von Gröbnerbasenbezüglich dieser Reduktionsrelationen zu entwickeln.
Zur Zeit haben Industrieroboter nur eine sehr begrenzte Wahrnehmung ihrer Umwelt. Wenn sich Menschen im Arbeitsraum des Roboters aufhalten sind sie daher gefährdet. Durch eine Einteilung der möglichen Roboterbewegung in verschiedene Klassen kann gezeigt werden, dass die für einen Menschen im Arbeitsraum gefährlichste Bewegung die freie Transferbewegung ist. Daher besteht die betrachtete Aufgabe darin, diese Transferbewegung eines Manipulators durchzuführen, ohne mit dynamischen Hindernissen, wie zum Beispiel Menschen, zu kollidieren. Das vorgestellte SIMERO-System realisiert eine globale Ganzarmkollisionsvermeidung auf der Basis von Bildern stationärer Kameras. Das System gliedert sich in die vier Hauptkomponenten Bildverarbeitung, Robotermodellierung, Kollisionserkennung und Bahnplanung. Diese Komponenten werden im einzelnen vorgestellt.
Die formale Spezifikation von Kommunikationssystemen stellt durch die mit ihr verbundene Abstraktion und Präzision eine wichtige Grundlage für die formale Verifikation von Systemeigenschaften dar. Diese Abstraktion begrenzt jedoch auch die Ausdrucksfähigkeit der formalen Beschreibungstechnik und kann somit zu problemunangemessenen Spezifikationen führen. Wir untersuchen anhand der formalen Beschreibungstechnik Estelle zunächst zwei solche Aspekte. Beide führen speziell in Hinsicht auf die Domäne von Estelle, der Spezifikation von Kommunikationsprotokollen, zu schwerwiegenden Beeinträchtigungen der Ausdrucksfähigkeit. Eines dieser Defizite zeigt sich bei dem Versuch, in Estelle ein offenes System wie z. B. eine Protokollmaschine oder einen Kommunikationsdienst zu spezifizieren. Da Estelle-Spezifikationen nur geschlossene Systeme beschreiben können, werden solche Komponenten immer nur als Teil einer fest vorgegebenen Umgebung spezifiziert und besitzen auch nur in dieser eine formale Syntax und Semantik. Als Lösung für dieses Problem führen wir die kompatible syntaktische und semantische Estelle-Erweiterung Open-Estelle ein, die eine formale Spezifikation solcher offener Systeme und ihres Imports in verschiedene Umgebungen ermöglicht. Ein anderes Defizit in der Ausdrucksfähigkeit von Estelle ergibt sich aus der strengen Typprüfung. Wir werden zeigen, dass es in heterogenen, hierarchisch strukturierten Kommunikationssystemen im Zusammenhang mit den dort auftretenden horizontalen und vertikalen Typkompositionen zu einer unangemessenen Modellierung von Nutzdatentypen an den Dienstschnittstellen kommt. Dieses Problem erweist sich beim Versuch einer generischen und nutzdatentypunabhängigen Spezifikation eines offenen Systems (z. B. mit Open-Estelle) sogar als fatal. Deshalb führen wir die kompatible Containertyp-Erweiterung ein, durch die eine formale Spezifikation nutzdatentypunabhängiger und somit generischer Schnittstellen von Diensten und Protokollmaschinen ermöglicht wird. Als Grundlage für unsere Implementierungs- und Optimierungsexperimente führen wir den „eXperimental Estelle Compiler“ (XEC) ein. Er ermöglicht aufgrund seines Implementierungskonzeptes eine sehr flexible Modellierung des Systemmanagements und ist insbesondere für die Realisierung verschiedener Auswahloptimierungen geeignet. XEC ist zudem mit verschiedenen Statistik- und Monitoring-Funktionalitäten ausgestattet, durch die eine effiziente quantitative Analyse der durchgeführten Implementierungsexperimente möglich ist. Neben dem vollständigen Sprachumfang von Estelle unterstützt XEC auch die meisten der hier eingeführten Estelle-Erweiterungen. Neben der Korrektheit ist die Effizienz automatisch generierter Implementierungen eine wichtige Anforderung im praktischen Einsatz. Hier zeigt sich jedoch, dass viele der in formalen Protokollspezifikationen verwendeten Konstrukte nur schwer semantikkonform und zugleich effizient implementiert werden können. Entsprechend untersuchen wir anhand des Kontrollflusses und der Handhabung von Nutzdaten, wie die spezifizierten Operationen effizient implementiert werden können, ohne das Abstraktionsniveau senken zu müssen. Die Optimierung des Kontrollflusses geschieht dabei ausgehend von der effizienten Realisierung der Basisoperationen der von XEC erzeugten Implementierungen primär anhand der Transitionsauswahl, da diese speziell bei komplexen Spezifikationen einen erheblichen Teil der Ausführungszeit bansprucht. Wir entwickeln dazu verschiedene heuristische Optimierungen der globalen Auswahl und der modullokalen Auswahl und werten diese sowohl analytisch wie auch experimentell aus. Wesentliche Ansatzpunkte sind dabei verschiedene ereignisgesteuerte Auswahlverfahren auf globaler Ebene und die Reduktion der zu untersuchenden Transitionen auf lokaler Ebene. Die Überprüfung der Ergebnisse anhand der ausführungszeitbezogenen Leistungsbewertung bestätigt diese Ergebnisse. Hinsichtlich der effizienten Handhabung von Daten untersuchen wir unterschiedliche Ansätze auf verschiedenen Ebenen, die jedoch in den meisten Fällen eine problemunangemessene Ausrichtung der Spezifikation auf die effiziente Datenübertragung erfordern. Eine überraschend elegante, problemorientierte und effiziente Lösung ergibt sich jedoch auf Basis der Containertyp-Erweiterung, die ursprünglich zur Steigerung des Abstraktionsniveaus eingeführt wurde. Dieses Ergebnis widerlegt die Vorstellung, dass Maßnahmen zur Steigerung der effizienten Implementierbarkeit auch immer durch eine Senkung des Abstraktionsniveaus erkauft werden müssen.
In dieser Arbeit wird gezeigt, wie durch eine Automatisierung von Software-Entwicklungsaktivitäten sowohl Effizienz- als auch Qualitätsgewinne erzielt und komplexe Aktivitäten beherrschbar gemacht werden können. Dazu wird zunächst eine solide Basis für eine modellbasierte Software-Entwicklung geschaffen. Nach der Identifikation der Probleme der bisher üblicherweise eingesetzten Metamodellierung wird eine verbesserte Multiebenenmodellierung vorgeschlagen, welche die explizite Angabe der Instanziierbarkeit (Tiefe und Automatismus der Instanziierung) der Modellelemente erlaubt und damit eine deutliche Vereinfachung und bessere Verständlichkeit der Metamodelle ermöglicht. Zur operationalen Beschreibung von Modelltransformationen im Kontext dieser Multiebenenmodellierung wird sodann die Aktionssprache AL++ konzipiert. Insbesondere durch die Einführung von Sprachelementen für die Handhabung von Relationen und Attributen und die Aufnahme von Reflexionskonstrukten in die Sprache AL++ werden Transformationen kompakt und generisch beschreibbar. Anwendung finden diese Ansätze in der modellbasierten Entwicklung reaktiver Systeme. Dazu wird eine existierende Entwicklungsmethode erweitert, um eine durchgängige Automatisierung realisieren zu können. Die wichtigste Erweiterung ist dabei die modifizierte Automatenmodellierung, bei welcher erweiterte Endliche Automaten durch die Komposition getrennt modellierter Zustandsübergänge spezifiziert werden, was eine eindeutige Verfolgbarkeit zu den Anforderungen erlaubt. Eingesetzt werden obige Techniken für die statische Analyse von Spezifikationen, wobei insbesondere die automatische Detektion von Feature-Interaktionen (also die Feststellung kritischer Wechselwirkungen zwischen Produktmerkmalen) in dieser Form erstmalig für den Bereich der reaktiven Systeme durchgeführt wird. Daneben werden automatisierte dynamische Analysen auf der Basis generierter Prototypen betrachtet. Die Analyseergebnisse können automatisiert für die Modifikation und Neukonstruktion der Prototypen genutzt werden, womit Software-Entwicklungsexperimente vollständig in einem „virtuellen Labor“ durchgeführt werden können. Wichtigstes experimentelles Ergebnis ist, dass eine statische Parametrisierung einer „intelligenten“ Temperaturregelung möglich ist und daher eine Reduktion der notwendigen Produktmerkmale (und damit der Komplexität) erreicht werden kann. In Fallstudien wird am Ende der Arbeit nachgewiesen, dass alleine durch die automatische Erzeugung von Entwicklungsdokumenten und die konsistente Änderung vorhergehender Dokumente durch die in dieser Arbeit implementierten Werkzeuge ein Effizienzgewinn von 54 % erreicht werden kann. Die Erstellung der eingesetzten Werkzeuge hätte sich dabei bereits nach zwei ähnlichen Projekten bezahlt gemacht.
Im Informationszeitalter haben die Menschen überall und jederzeit Zugang zu einer kontinuierlich ansteigenden Fülle von Informationen. Hierzu trägt vor allem die explosionsartig wachsende globale Vernetzung der Welt, insbesondere das Internet, maßgeblich bei. Die Transformation der verfügbaren Informationen in Wissen sowie die effiziente Nutzung dieses Wissens stellen dabei entscheidende Faktoren für den Erfolg eines Unternehmens oder eines Einzelnen dar. Es stellt sich also die Frage: Leben wir im Informationszeitalter? Diese Frage erinnert an die von Immanuel Kant in [65] gestellte Frage "Leben wir jetzt in einem aufgeklärten Zeitalter?" und dessen Antwort "Nein, aber wohl in einem Zeitalter der Aufklärung.". Entsprechend lässt sich auch die Frage "Leben wir in einem informierten Zeitalter?" mit "Nein, aber wohl in einem Zeitalter der Information" beantworten (vergleiche [14]). Das Problem, dass sich die überwältigende Fülle an Information ohne geeignete Hilfsmittel vom Menschen nicht oder nur schwer beherrschen lässt, hat im Laufe des letzten Jahrzehnts maßgeblich zur Entwicklung des äußerst dynamischen Forschungs- und Anwendungsgebietes der Visualisierung als Teilgebiet der Computergrafik beigetragen. Der Grund hierfür liegt in der Tatsache, dass der Mensch wesentlich besser mit visuellen Eindrücken als mit abstrakten Zahlen oder Fakten umgehen kann. Die Erkennung von Mustern in Daten (z. B. Gruppierungen und Häufungen) wird durch die Visualisierung stark vereinfacht und lässt vielmals Zusammenhänge zwischen Daten überhaupt erst greifbar werden. Unter computergestützter Visualisierung versteht man die in der Regel interaktive grafische Umsetzung von Daten. Handelt es sich dabei um physikalische Daten (z. B. entstanden durch Messvorgänge), so spricht man von Scientific Visualization. Handelt es sich eher um abstrakte bzw. nicht-physikalische Daten, so ordnet man die entsprechenden Verfahren der Information Visualization zu. Beide Teilgebiete der Visualisierung verfolgen jedoch das gemeinsame Ziel, Informationen dem Menschen sichtbar und verständlich zu machen und verwenden hierzu geeignete visuelle Paradigmen, häufig verbunden mit entsprechenden Interaktionsmöglichkeiten. Die vorliegende wissenschaftliche Arbeit ist in den Bereich der angewandten Computergrafik, speziell der interaktiven Visualisierung, einzuordnen. Die primären Ziele lagen dabei in der Übertragung des Begriffes kontextsensitiv auf den Bereich der Visualisierung zur Sicherstellung effizienter und kontextsensitiver Visualisierungsapplikationen sowie die Anwendung in aktuellen praktischen Aufgabenstellungen. Die Umsetzung einer kontextsensitiven Visualisierung gelingt im Rahmen dieser Arbeit durch die zukunftsweisende Kopplung von Visualisierungspipeline und Agententechnologie. Basierend auf der Identifikation zentraler Szenarien der kontextsensitiven Visualisierung wird eine agentenbasierte Visualisierungskontrolle durch intelligente Überwachung und Regelung der Visualisierungspipeline vorgestellt. Nach einer Zusammenfassung der relevanten Grundlagen aus den Gebieten der Visualisierung und der Agententechnologie folgen eine theoretische Klassifizierung und ein Überblick über existierende Systeme und Anwendungen aus beiden Bereichen. Anschließend wird das im Rahmen dieser Arbeit erarbeitete Paradigma der kontextsensitiven Visualisierung vorgestellt und die praktische, komponentenbasierte Umsetzung erläutert. Einen nicht unerheblichen Anteil der Arbeit machen drei innovative, auf der kontextsensitiven Visualisierung basierende Visualisierungsapplikationen aus, welche die Möglichkeiten und die Funktionsfähigkeit der entwickelten Architektur aufzeigen. Die Entwicklung einer plattformunabhängigen interaktiven Visualisierung beschäftigt sich insbesondere mit dem Auffinden der aktuell maximal möglichen Performance durch Abwägung der gegenläufigen Hauptparameter Qualität und Interaktivität und behandelt damit vor allem den System- und Interaktionskontext. Der Gedanke der plattformunabhängigen interaktiven Visualisierung wird anschließend auf mobile Informationssysteme ausgeweitet. Hier ist neben den Performanceaspekten vor allem die Art des Ausgabemediums, d. h. der Darstellungskontext, ein entscheidender Faktor. Die dritte Anwendung stellt eine agentenbasierte Applikation für die Bekleidungsindustrie in Form eines interaktiven Individual-Katalogs dar und behandelt insbesondere den Daten- und den Benutzerkontext. Eine kurze Zusammenfassung sowie ein Ausblick auf geplante zukünftige Entwicklungen runden letztlich die Betrachtungen ab.
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.
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.