Erfahrungsmanagement (EM) ist eine Spezialform des Wissensmanagements, die sich mit aufgabenbezogenem Wissen beschäftigt. Diese Arbeit entwickelt ein Rahmenwerk für Assistenzsysteme, die Menschen bei EM-Aufgaben unterstützen. Es untersucht nicht nur technische Fragen (Erfahrungswissen sammeln, strukturieren, speichern und wiederverwenden) sondern auch organisatorische (Erfahrungswissen evaluieren und pflegen) und psychosoziale Aspekte (ein EM-System integrieren, Barrieren vermeiden, den Systemeinsatz bewerten). Fallbasierte Anwendungsbeispiele für industrielle und experimentelle Szenarien zeigen, welche Prozesse wo unterstützt oder gar teilautomatisiert werden können. Sie dienen der experimentellen Evaluierug der Fragen, die ich zu Beginn jedes Anwendungskapitels formuliert habe. / Experience Management (EM) is a special form of Knowledge Management that deals with task-based knowledge. This thesis provides a framework for assistant systems that support human beings in EM tasks. It deals not only with technical issues (how to collect, structure, store, retrieve, and reuse experiential knowledge), but als with organizational issues (how to evaluate and maintain it) and psychosocial questions (how to integrate an EM system, how to avoid barriers, how to evaluate the success of the whole system). Case-based sample applications from both, industrial and experimental scenarios, show to what extend the particular EM processes can be supported or which sub-processes can even be automated. By means of experiments with these implemented samples, we evaluate the topics that are discussed at the beginning of each application chapter.

Fotorealistisches Rendering ist eines der Hauptziele der Computer Grafik. Mittels physikalischer Simulation ist eine fotorealistische Darstellung immer noch rechenaufwändig. Diese Arbeit stellt neue Methoden für Bild-basiertes Rendering komplexer Objekte am Beispiel von Kleidung vor. Die vorgestellten Methoden nutzen Kamerabilder und deren fotorealistische Eigenschaften für komplexe Animationen und Texturmodifikationen. Basierend auf der Annahme, dass für eng anliegende Kleidung Faltenwurf hauptsächlich von der Pose des Trägers beeinflusst wird, schlägt diese Dissertation ein neues Bild-basiertes Verfahren vor, das neue Bilder von Kleidungsstücken abhängig von der Körperpose einer Person aus einer Datenbank von Bildern synthetisiert. Posen-abhängige Eigenschaften (Textur und Schattierung) werden über Abbildungsvorschriften zwischen den Bildern extrahiert und im Posenraum interpoliert. Um die Erscheinung eines Objekts zu verändern, wird ein Verfahren vorgestellt, das den Austausch von Texturen ohne Kenntnis der zugrundeliegenden Szeneneigenschaften ermöglicht. Texturdeformation und Schattierung werden über Bildregistrierung zu einem geeigneten Referenzbild extrahiert. Im Gegensatz zu klassischen Bild-basierten Verfahren, in denen die Synthese auf Blickpunktänderung beschränkt und eine Veränderung des Objekts nicht möglich ist, erlauben die vorgestellten Verfahren komplexe Animationen und Texturmodifikation. Beide Verfahren basieren auf örtlichen und photometrischen Abbildungen zwischen Bildern. Diese Abbildungen werden basierend auf einem angepassten Brightness Constancy Constraint mit Gitternetz-basierten Modellen optimiert. Die vorgestellten Verfahren verlagern einen großen Teil des Rechenaufwands von der Darstellungsphase in die vorangegangene Trainingsphase und erlauben eine realistische Visualisierung von Kleidung inklusive charakteristischer Details, ohne die zugrundeliegenden Szeneneigenschaften aufwändig zu simulieren. / One principal intention of computer graphics is the achievement of photorealism. With physically-based methods, achieving photorealism is still computationally demanding. This dissertation proposes new approaches for image-based visualization of complex objects, concentrating on clothes. The developed methods use real images as appearance examples to guide complex animation or texture modification processes, combining the photorealism of images with the ability to animate or modify an object. Under the assumption that wrinkling depends on the pose of a human body (for tight-fitting clothes), a new image-based rendering approach is proposed, which synthesizes images of clothing from a database of images based on pose information. Pose-dependent appearance and shading information is extracted by image warps and interpolated in pose-space using scattered data interpolation. To allow for appearance changes in image-based methods, a retexturing approach is proposed, which enables texture exchange without a-priori knowledge of the underlying scene properties. Texture deformation and shading are extracted from the input image by a warp to an appropriate reference image. In contrast to classical image-based visualization methods, where animation is restricted to viewpoint change and appearance modification is not possible, the proposed methods allow for complex pose animations and appearance changes. Both approaches build on image warps, not only in the spatial but also in the photometric domain. A new framework for joint spatial and photometric warp optimization is introduced, which estimates mesh-based warp models under a modified brightness constancy assumption. The presented approaches shift computational complexity from the rendering to an a-priori training phase and allow a photo-realistic visualization and modification of clothes, including fine and characteristic details without computationally demanding simulation of the underlying scene and object properties.

Trotz der Entwicklungen der letzten Jahre kommt es in der Robotik immer noch vor, dass mobile Roboter scheinbar sinnlose Handlungen ausführen. Der Grund für dieses Verhalten ist oftmals, dass sich das interne Weltbild des Roboters stark von der tatsächlichen Situation, in der sich der Roboter befindet, unterscheidet. Die darauf basierende Robotersteuerung wählt infolge dieser Diskrepanz scheinbar sinnlose Handlungen aus. Eine wichtige Ursache von Lokalisierungsfehlern stellen Kollisionen des Roboters mit anderen Robotern oder seiner Umwelt dar. Mit Hilfe eines Hindernismodells wird der Roboter in die Lage versetzt, Hindernisse zu erkennen, sich ihre Position zu merken und Kollisionen zu vermeiden. Ferner wird in dieser Arbeit eine Erweiterung der Bewegungsmodellierung beschrieben, die die Bewegung in Mobilitätszustände untergliedert, die jeweils ein eigenes Bewegungsmodell besitzen und die mit Hilfe von Propriozeption unterschieden werden können. Mit Hilfe der Servo-Motoren des Roboters lässt sich eine Art Propriozeption erzielen: der momentan gewünschte, angesteuerte Gelenkwinkel wird mit dem tatsächlich erreichten, im Servo-Motor gemessenen Winkel verglichen. Dieser "Sinn" erlaubt eine bessere Beschreibung der Roboterbewegung. Verbesserung des Sensormodells wird das bisher wenig untersuchte Konzept der Negativinformation, d.h. das Ausbleiben einer erwarteten Messung, genutzt. Bestehende Lokalisierungsansätze nutzen diese Information nicht, da es viele Gründe für ein Ausbleiben einer erwarteten Messung gibt. Eine genaue Modellierung des Sensors ermöglicht es jedoch, Negativinformation nutzbar zu machen. Eine Weltmodellierung, die Negativinformation verarbeiten kann, ermöglicht eine Lokalisierung des Roboters in Situationen, in denen einzig auf Landmarken basierende Ansätze scheitern. / Despite the dramatic advancements in the field of robotics, robots still tend to exhibit erratic behavior when facing unexpected situations, causing them, for example, to run into walls. This is mainly the result of the robot''s internal world model no longer being an accurate description of the environment and the robot''s localization within the environment. The key challenge explored in this dissertation is the creation of an internal world model for mobile robots that is more robust and accurate in situations where existing approaches exhibit a tendency to fail. First, means to avoid a major source of localization error - collisions - are investigated. Efficient collision avoidance is achieved by creating a model of free space in the direct vicinity of the robot. The model is based on camera images and serves as a short term memory, enabling the robot to avoid obstacles that are out of sight. It allows the robot to efficiently circumnavigate obstacles. The motion model of the robot is enhanced by integrating proprioceptive information. Since the robot lacks sensors dedicated to proprioception, information about the current state and configuration of the robot''s body is generated by comparing control commands and actual motion of individual joints. This enables the robot to detect collisions with other robots or obstacles and is used as additional information for modeling locomotion. In the context of sensing, the notion of negative information is introduced. Negative information marks the ascertained absence of an expected observation in feature-based localization. This information is not used in previous work on localization because of the several reasons for a sensor to miss a feature, even if the object lies within its sensing range. This information can, however, be put to good use by carefully modeling the sensor. Integrating negative information allows the robot to localize in situations where it cannot do so based on landmark observation alone.

Performanz ist ein zentraler Bestandteil des Designs von Anonymisierungsdiensten. Ihre zunehmende Popularität führt jedoch zu einer hohen Netzwerklast, die unzulängliche Entwurfsentscheidungen imminent macht. Die Anforderungen und die vielschichtige Architektur von Anonymisierungsdiensten machen die Thematik zu einem anspruchsvollen und zugleich inspirierenden Forschungsgegenstand. Die vorliegende Arbeit diskutiert das Design von sogenannten Niedriglatenz-Anonymisierungsdiensten im Allgemeinen und dem Tor-Netzwerk als relevantesten Vertreter im Speziellen. Es werden Lösungen für eine Reihe von Forschungsfragen entwickelt, die allesamt das Ziel verfolgen, diese Overlay-Netzwerke zu verbessern und sicherer zu gestalten. Es entsteht ein fundamentales Verständnis zu Netzwerkaspekten in Anonymisierungs-Overlays, das die Netzwerklast, als vorherrschende Ursache für die schwache Performanz, thematisiert. / Performance is a pivot point in the design of anonymity overlays. Due to their growing popularity, they are faced with increasing load, which makes design problems imminent. The special requirements and complex architecture of anonymity overlays renders the topic a challenging but likewise inspiring object of research. In this work, we discuss the design of low-latency anonymous communication systems in general and the Tor network as the de-facto standard in particular. We develop solutions to a number of research questions, all collectively following the aim of enhancing and securing such networks. By doing this we create a fundamental technical understanding of networking aspects in anonymity overlays and tackle the most prevalent performance issue experienced today: network congestion.

Eine Zeitreihe ist eine zeitlich geordnete Folge von Datenpunkten. Zeitreihen werden typischerweise über Sensormessungen oder Experimente erfasst. Sensoren sind so preiswert geworden, dass sie praktisch allgegenwärtig sind. Während dadurch die Menge an Zeitreihen regelrecht explodiert, lag der Schwerpunkt der Forschung in den letzten Jahrzehnten auf der Analyse von (a) vorgefilterten und (b) kleinen Zeitreihendatensätzen. Die Analyse realer Zeitreihendatensätze wirft zwei Probleme auf: Erstens setzen aktuelle Ähnlichkeitsmodelle eine Vorfilterung der Zeitreihen voraus. Das beinhaltet die Extraktion charakteristischer Teilsequenzen und das Entfernen von Rauschen. Diese Vorverarbeitung muss durch einen Spezialisten erfolgen. Sie kann zeit- und kostenintensiver als die anschließende Analyse und für große Datensätze unrentabel werden. Zweitens führte die Verbesserung der Genauigkeit aktueller Ähnlichkeitsmodelle zu einem unverhältnismäßig hohen Anstieg der Komplexität (quadratisch bis biquadratisch). Diese Dissertation behandelt beide Probleme. Es wird eine symbolische Zeitreihenrepräsentation vorgestellt. Darauf aufbauend werden drei verschiedene Ähnlichkeitsmodelle eingeführt. Diese erweitern den aktuellen Stand der Forschung insbesondere dadurch, dass sie vorverarbeitungsfrei, unempfindlich gegenüber Rauschen und skalierbar sind. Anhand von 91 realen Datensätzen und Benchmarkdatensätzen wird zusätzlich gezeigt, dass die hier eingeführten Modelle auf den meisten Datenätzen die höchste Genauigkeit im Vergleich zu 15 aktuellen Ähnlichkeitsmodellen liefern. Sie sind teilweise drei Größenordnungen schneller und benötigen kaum Vorfilterung. / A time series is a collection of values sequentially recorded from sensors or live observations over time. Sensors for recording time series have become cheap and omnipresent. While data volumes explode, research in the field of time series data analytics has focused on the availability of (a) pre-processed and (b) moderately sized time series datasets in the last decades. The analysis of real world datasets raises two major problems: Firstly, state-of-the-art similarity models require the time series to be pre-processed. Pre-processing aims at extracting approximately aligned characteristic subsequences and reducing noise. It is typically performed by a domain expert, may be more time consuming than the data mining part itself, and simply does not scale to large data volumes. Secondly, time series research has been driven by accuracy metrics and not by reasonable execution times for large data volumes. This results in quadratic to biquadratic computational complexities of state-of-the-art similarity models. This dissertation addresses both issues by introducing a symbolic time series representation and three different similarity models. These contribute to state of the art by being pre-processing-free, noise-robust, and scalable. Our experimental evaluation on 91 real-world and benchmark datasets shows that our methods provide higher accuracy for most datasets when compared to 15 state-of-the-art similarity models. Meanwhile they are up to three orders of magnitude faster, require less pre-processing for noise or alignment, or scale to large data volumes.

Gegenstand der Arbeit ist die Verifikation von verteilten diskreten Systemen in bezug auf Spezifikationen ihres Verhaltens. Diskrete Systeme bestehen aus einer abzaehlbaren Zustandsmenge und einer Zustandsuebergangsrelation. Bei verteilten Systemen ist eine signifikante Zahl von Zustandsuebergaengen nur durch eine kleine Zahl von Komponenten eines strukturierten Zustandsraumes bedingt und aendert auch nur wenige Komponenten. Bei praktisch relevanten Systemen ist die Zustandszahl unbeherrschbar gross. Dieses Phaenomen wird Zustandsraumexplosion genannt. Verteiltheit gilt als eine der wesentlichen Ursachen fuer Zustandsraumexplosion, weil nebenlaeufig moegliche lokale Zustandsuebergaenge abhaengig von ihren exponentiell vielen Ausfuehrungsreihenfolgen exponentiell viele verschiedene Zwischenzustaende erzeugen koennen. Fuer Verifikationsaufgaben sind Systeme daher implizit gegeben durch eine Beschreibung von Anfangszustaenden und (lokale) Regeln zur Generierung von Folgezustaenden. Solche Systembeschreibungen folgen verschiedenen Paradigmen, z.B. dem variablenorientierten Paradigma (Zustaende sind Werte von Variablen, die durch Zustandsuebergaenge gelesen und geschrieben werden) oder dem ressourcenorientierten Paradigma (Zustaende sind Verteilungen von Ressourcen im System, die durch Zustandsuebergaenge konsumiert oder produziert werden). Die Verfuegbarkeit von Verifikationstechniken oder spezifischen Implementationen haengt vom zugrundeliegenden Paradigma ab. Als Sprache zur Formulierung von Spezifikationen des Verhaltens verwenden wir etablierte temporale Logiken und fuer die Praxis bedeutsame Fragmente solcher Logiken. Temporale Logik beschreibt Eigenschaften von Abfolgen von Zustaenden, basierend auf elementaren, einzelne Zustaende betreffenden Eigenschaften. Auf einer expliziten Systemdarstellung lassen sich temporallogische Eigenschaften effizient, d.h. mit einer linear von der Zustandszahl abhaengigen Laufzeit, verifizieren. Eine solche Verifikation basiert auf einfachen Suchalgorithmen in dem durch das System definierten Zustandsgraph. Ein solcher Verifikationsansatz ist aber wegen der genannten Zustandsraumexplosion nicht durchfuehrbar. Im wesentlichen werden drei Loesungsansaetze in Richtung durchfuehrbarer Verifikationsalgorithmen verfolgt. Die strukturelle Verifikation versucht, Eigenschaften direkt aus spezifischen Mustern in der impliziten Systembeschreibung abzuleiten. Der derzeitige Stand der Technik gestattet solche Ableitungen nur fuer wenige und einfach strukturierte Verhaltensspezifikationen und erfordert auch dann in einigen Faellen recht aufwendige Berechnungen. Bei der symbolischen Zustandsraumanalyse wird der Zustandsraum erschoepfend durchmustert, allerdings unter Benutzung von Datenstrukturen, deren elementare Objekte ganze Mengen von Zustaenden beschreiben, und deren elementare Operationen die Folgezustaende fuer ganze solche Mengen aus der impliziten Systembeschreibung errechnen. Bei der expliziten Zustandsraumverifikation, dem Thema der vorliegenden Habilitationsschrift, wird eine explizite Repraesentation eines Zustandsraumes generiert, der wesentlich kleiner ist als der Zustandsraum des untersuchten Systems, in bezug auf die untersuchte Eigenschaft aber per Konstruktion aequivalent zum originalen System ist. Zur Konstruktion werden Informationen aus der impliziten Systembeschreibung herangezogen. Eine Technologie zur expliziten Zustandsraumverifikation besteht also aus - Einer mathematisch fundierten Theorie, die einer bestimmten Konstruktionsmethode bescheinigt, welche Eigenschaften durch sie bewahrt werden; - effizienten Algorithmen zur Implementation eine solchen Konstruktion; Die Arbeit enthaelt, fuer mehrere bekannte Verfahren, Beitraege zu jeweils mindestens einem der beiden Bestandteile einer expliziten Zustandsraumverifikationstechnik. Die Methode der sturen Mengen verkleinert den explizit zu konstruierenden Zustandsraum dadurch, dass von den in einem Zustand moeglichen Zustandsuebergaengen nur einige tatsaechlich untersucht werden, so dass weit weniger Zwischenzustaende durch verschiedene Abfolge nebenlaeufiger lokaler Zustandsuebergaenge entstehen. Die zu untersuchenden Uebergaenge werden abhaengig von der zu verifizierenden Eigenschaft und Informationen aus der Systemstruktur so ausgewaehlt, dass zu jeder Klasse von fuer die Eigenschaft relevanten Systemablaeufen wenigstens einer im reduzierten Zustandsraum repraesentiert ist. Die erste 1988 veroeffentlichte Methode diente der Bewahrung von terminalen Zustaenden sowie mindestens eines Pfades unendlicher Laenge. In der Folge wurde diese Technik auf viele andere Klassen von Eigenschaften erweitert, wobei vor allem die Faehigkeit, einen unendlichen Pfad zu bewahren, dahingehend verfeinert wurde, dass gezielt Pfade mit bestimmten Eigenschaften bewahrt werden konnten. Dabei spielte das Konzept unsichtbarer Zustandsuebergaenge eine tragende Rolle, wobei ein unsichtbarer Zustandsuebergang die Eigenschaft hat, dass er keine fuer die Eigenschaft relevanten Zustandskomponenten aendert. Daher war die Anwendung der Methode sturer Mengen begrenzt auf lokale Systemeigenschaften, weil andereseits zu wenige unsichtbare Uebergaenge fuer eine substantielle Reduktion zur Verfuegung stuenden. In der vorliegenden Arbeit setzen wir an der ersten Arbeit zur Methode sturer Mengen an und verfeinern die Faehigkeit, terminale Zustaende zu bewahren, dahingehend, dass nun die Praesenz von Zustaenden mit beliebigen in temporaler Logik formulierbaren Eigenschaften bewahrt werden. Die neue Methode basiert nicht auf der Existenz unsichtbarer Uebergaenge und kann in der Tat auch bei der Verifikation globaler Systemeigenschaften zu substantieller Reduktion fuehren. Das neue Konzept zur Konstruktion des reduzierten Zustandsraumes sind sogenannte UP-Mengen. Eine UP-Menge ist eine Menge von Uebergaengen, von denen mindestens einer in einem Systemablauf von einem Zustand, der die untersuchte Eigenschaft nicht erfuellt, zu einem Zustand, der die Eigenschaft erfuellt, vorkommen muss. Wir geben Algorithmen an, die kleine UP-Mengen fuer beliebige Zustaende aus der impliziten Systembeschreibung und einer Repraesentation der untersuchten Eigenschaft in der temporalen Logik CTL berechnet. Wir zeigen, dass jede Konstruktion, die in einem Zustand alle Uebergaenge in einer schwach sturen Obermenge einer zu dem Zustand berechneten UP-Menge untersucht, alle Zustaende erreicht, die die Eigenschaft besitzen. Dabei ist die Konstruktion schwach sturer Mengen die allen Methoden sturer Mengen gemeinsame Grundkonstruktion. Symmetrische Reduktion verkleinert den zu untersuchenden Zustandsraum dadurch, dass zu jeder Klasse von in bezug auf Symmetrie aequivalenten Zustaenden jeweils nur einer weiterverfolgt wird. Dadurch lassen sich alle gegenueber Symmetrie insensitive Eigenschaften bewahren (wobei man oft Insensitivitaet einer Eigenschaft durch die geeignete Wahl der Symmetrienmenge erreichen kann). Symmetrische Reduktion beinhaltet zwei Probleme, erstens das Aufinden der einem System innewohnenden Symmetrie, und zweitens, zu einem gegebenen Zustand, das Auffinden zu ihm aequivalenter Zustaende in der Menge bereits untersuchter Zustaende. Die meisten vorhandenen Implementationen leiten Symmetrien aus speziellen Datenstrukturen ab, in denen wegen der eingeschraenkten Operationen die verschiedenen Elemente des Typs austauschbar sind. Das Auffinden aequivalenter Zustaende wird durch eine Transformation neu berechnter Zustaende in einen aequivalenten kanonischen Repraesentanten realisert. Alternativ zu diesem Ansatz wurde zur Beschreibung von Symmetrien die Verwendung von Graphautomorphismen auf netzartigen impliziten Systembeschreibungsformen vorgeschlagen. Es zeigt sich, dass per Umwandlung von Datenabhaengigkeiten in Graphrepraesentationen, jede Datentypsymmetrie auch einen Graphautomorphismus bildet, andererseits aber durch Graphautomorphismen Symmetrien beschreibbar sind, die sich in Datentypbetrachtungen nicht wiederfinden lassen. Diese zusaetzlichen Symmetrien erlauben eine staerkere Reduktion des Zustandsraumes. Zur Graphautomorphismentechnik fehlten bislang leistungsfaehige Algorithmen zur Umsetzung dieser Technologie. Wir setzen an der auf Graphautomorphismen basierenden Methode an und unterlegen alle Teilprobleme mit leistungsfaehigen Algorithmen. Die Berechnung der Automorphismen beschraenken wir auf ein Erzeugendensystem, das polynomiell viele Elemente, gemessen an der Groesse der impliziten Systembeschreibung, hat. Die Berechnung selbst ist schlimmstenfalls exponentiell, was nicht verwundert, weil das Problem mit einem Entscheidungsproblem eng korreliert, von dem bekannt ist, dass es in der Klasse NP, aber unbekannt, ob es NP-vollstaendig oder in P liegt. Diese Eigenschaft hat dem Problem eingehende Untersuchung zuteil werden lassen, wegen der nach wie vor offenen "P ungleich NP?"-Frage. Trotzdem ist kein polynomieller Algorithmus bekannt. Umso erfreulicher ist es, dass unser Berechnungsalgorithmus sich auf realistischen Beispielen bisher durchweg polynomiell verhielt, und lediglich bei eigens konstruierten Systemen ins Exponentielle ausriss. Fuer die Loesung des Problems, aequivalente bereits bekannte Zustaende aufzuspueren, schlagen wir mehrere Techniken vor und beschreiben ihre Leistungsfaehigkeit abhaengig von der Struktur der innewohnenden Symmetrie. Fuer duenne Symmetriegruppen (wenige symmetrische Transformationen) eignet sich eine Technik, bei der die Symmetrien der Reihe nach aus dem Erzeugendensystem generiert werden, und das symmetrische Bild des neuen Zustandes mit der Menge der bekannten Zustaende verglichen wird. Dabei koennen wir, abhaengig vom Ausgang einer solchen Ueberpruefung, die Generierung von Symmetrien unterdruecken, von denen aus vorhandenen Informationen klar ist, dass sie keinesfalls zum Erfolg fuehren. Dadurch kann eine erhebliche Effizienzsteigerung erzielt werden. Bei einer zweiten Technik iterieren wir die bekannten Zustaende, genauer gesagt, diejenigen Zustaende, die fuer eine die Symmetrie respektierende Hashfunktion denselben Wert liefert wie der neue Zustand, ob es eine Symmetrie gibt, die beide Zustaende ineinander ueberfuehrt. Das verbleibende Problem kann durch eine Adaption des Symmetrieberechnungsverfahrens geloest werden. Eine vorherige Berechnung des Erzeugendensystems kann entfallen. Die dritte vorgeschlagene Technik benutzt das Erzeugendensystem, um den neuen Zustand approximativ in einen kanonischen aequivalenten Zustand zu ueberfuehren. Diese Technik ist von allen beschriebenen Methoden die effizienteste, liefert aber groessere Zustandsraeume als die beiden anderen Techniken. Wir studieren die Vor- und Nachteile aller Techniken anhand mehrerer Beispielsysteme. Die dritte in der Arbeit behandelte Technik ist die Methode der Ueberdeckbarkeitsgraphen. Sie ist spezifisch fuer die ressourcenbasierte Systembeschreibungsform der Petrinetze. Sie diente urspruenglich zur Aufspuerung von Stellen im System, an denen sich unbeschraenkt viele Ressourcen ansammeln koennen. Formal ist ein Ueberdeckbarkeitsgraph eine endliche Abstraktion eines Systems mit bis zu unendlich vielen Zustaenden. Von nur wenigen Eigenschaften war bekannt, dass sie sich aus dem Ueberdeckbarkeitsgraphen ableiten lassen. Wir formulieren Regeln zur Auswertung von Ueberdeckbarkeitsgraphen, mit deren Hilfe es moeglich ist, eine Vielzahl von in temporaler Logik formulierten Eigenschaften aus dem Ueberdeckbarkeitsgraph abzuleiten. Diese Reglen sind inhaerent unvollstaendig, da bekannt ist, dass fuer viele Eigenschaften es Paare von Systemen gibt, die isomorphe Ueberdeckbarkeitsgraphen liefern, sich aber in bezug auf die Eigenschaft verschieden verhalten. Fuer universelle Eigenschaften des CTL-Fragments ACTL erhalten wir Bewahrungsresultate durch das Ausweisen einer Simulationsrelation zwischen dem originalen System und seinem Ueberdeckbarkeitsgraph. Fuer existentielle Eigenschaften basieren unsere Resultate auf einer Abschwaechung der Erfuellbarkeitsrelation ueber Zustaenden des Ueberdeckbarkeitsgraphen. Einem Zustand des Ueberdeckbarkeitsgraphen entsprechen divergierende Folgen von Zustaenden des Originalgraphen. Normalerweise schreibt man einem Zustand des Ueberdeckbarkeitsgraphen dann eine Eigenschaft zu, wenn alle Folgenglieder im Originalsystem die Eigenschaft besitzen. Wir arbeiten dagegen mit einem Begriff, wo Gueltigkeit der Eigenschaft nur fuer fast alle Folgenglieder gefordert wird. Eine letzte Gruppe von Techniken ist bisher in der Zustandsraumverifikation nicht eingestzt worden, aber aus der strukturellen Verifikation fuer Petrinetze bekannt. Zu einem Petrinetz kann eine ganzzahlige Inzidenzmatrix C gebildet werden, mit deren Hilfe ein linear-algebraischer Zusammenhang zwischen voneinander errichbaren Zustaenden hergestellt werden kann. Stellen- und Transitionsinvarianten sind Loesungen der durch C-T bzw. C definierten homogenen Gleichungssysteme. Dabei dienen Stelleninvarianten gewoehnlich einer Abschaetzung der Menge der erreichbaren Zustaende nach oben, mit daraus resultierenden Moeglichkeiten der Ableitung von Eigenschaften, waehrend Transitionsinvarianten Zyklen im Zustandsraum charakterisieren. Wir verwenden Stelleninvarianten zur Kompression von einzelnen Zustaenden. Durch Stelleninvarianten lassen sich einige Komponenten in einen funktionalen Zusammenhang zu den verbleibenden Komponenten stellen. Dadurch ist auch nach dem Streichen der funktional abhaengigen Stellen der Zustand noch eindeutig determiniert. Wir zeigen, dass bei der Konstruktion des Zustandsraumes ein durch die verbleibenden Stellen gebildeter "Fingerabdruck" ausreicht. Transitionsinvarianten verwenden wir dazu, eine Menge von Zustaenden so auszuzeichnen, dass jeder Zyklus im Zustandsraum mindestens einen ausgezeichneten Zustand enthaelt. Darufhin speichern wir noch noch ausgezeichnete Zustaende permanent, sparen also Speicherplatz. Fuer nicht ausgezeichnete Zustaende kann es passieren, dass sie mehrmals aufgesucht werden (auf verschiedene Weise aus Vorgaengerzustaenden entstehen). Weil sie nicht gespeichert sind, werden auch wiederholt ihre Nachfolgezustaende untersucht. Da in jedem Kreis mindestens ein ausgezeichneter, also permanent zu speichernder Zustand enthalten ist, entstehen durch diese wiederholte Berechnung keine Probleme in bezug auf Terminierung des Verfahrens, wohl aber erhebliche Laufzeiteinbussen. Wir schlagen Methoden zur Begrenzung der Laufzeiteinbussen um den Preis weiterer zu speichernder Zustaende vor. Fuer alle untersuchten Methoden studieren wir die Abhaengigkeit der Anwendbarkeit und Effizienz der Methode von dem der gegebenen impliziten Systembeschreibung zugrundeliegenden Paradigma. Wir untersuchen ebenfalls die Kompatibilitaet der Verfahren mit verschiedenen Strategien zur Generierung des Zustandsraumes (Tiefe zuerst, Breite zuerst, verteilt) und Moeglichkeiten der gemeinsamen Anwendung verschiedener Techniken. / Verification is the task of determining whether a (model of a) system holds a given behavioral property. State space verification comprises a class of computer aided verification techniques where the property is verified through exhaustive exploration of the reachable states of the system. Brute force implementations of state space verification are intractable, due to the well known state explosion problem. Explicit state space verification techniques explore the state space one state at a time, and rely usually on data structures where the size of the data structure increases monotonously with an increasing number of explored states. They alleviate state explosion by constructing a reduced state space that, by a mathematically founded construction, behaves like the original system with respect to the specified properties. Thereby, decrease of the number of states in the reduced system is the core issue of a reduction technique thus reducing the amount of memory required. An explicit state space verification technique comprises of - a theory that establishes whether, and how, certain properties can be preserved through a construction of a reduced state space; - a set of procedures to execute the actual construction efficiently. In this thesis, we contribute to several existing explicit state space verification techniques in either of these two respects. We extend the class of stubborn set methods (an instance of partial order reduction) by constructions that preserve previously unsupported classes of properties. Many existing constructions rely on the existence of "invisible" actions, i.e. actions whose effect does not immediately influence the verified property. We propose efficient constructions that can be applied without having such invisible actions, and prove that they preserve reachability properties as well as certain classes of more complex behavioral system properties. This way, so called "global" properties can now be approached with better stubborn set methods. We pick up a graph automorphism based approach to symmetry reduction and propose a set of construction algorithms that make this approach feasible. In difference to established symmetry techniques that rely on special "symmetry creating" data types, a broader range of symmetries can be handled with our approach thus obtaining smaller reduced state spaces. Coverability graph construction leads to a finite representation of an infinite state space of a Petri net by condensing diverging sequences of states to their limit. We prove rules to determine temporal logic properties of the original system from its coverability graph, far beyond the few properties known to be preserved so far. We employ the Petri net concept of linear algebraic invariants for compressing states as well as for leaving states out of explicit storage. Compression uses place invariants for replacing states by smaller fingerprints that still uniquely identify a state (unlike many hash compression techniques). For reducing the number of explicitly stored states, we rely on the capability of Petri net transition invariants to characterize cycles in the state space. For termination of an exhaustive exploration of a finite state space, it is sufficient to cover all cycles with explicitly stored states. Both techniques are easy consequences of well known facts about invariants. As a novel contribution, we observe that both techniques can be applied without computing an explicit representation of (a generating set for) the respective invariants. This speeds up the constructions considerably and saves a significant amount of memory. For all presented techniques, we illustrate their capabilities to reduce the complexity of state space reduction using a few academic benchmark examples. We address compatibility issues, i.e. the possibility to apply techniques in combination, or in connection with different strategies for exploring the reduced state space. We propose a scheme to distribute state space exploration on a cluster of workstations and discuss consequences for using this scheme for state space reduction. We collect observations concerning the impact of the choice of system description formalisms, and property specification languages, on the availability of explicit state space verification techniques.

Unter dem Evolutionsprozeß eines Objekts, das aus einer gegebenen Klasse zufällig ausgewählt wird, versteht man das folgende Gedankenexperiment. Zu einem geeigneten Parameter der Objekte der Klasse betrachtet man die Teilklasse derjenigen Objekte, bei denen dieser Parameter einen bestimmten Wert x annimmt. Dadurch stellen sich die folgenden Fragen: Wie sieht ein typisches Objekt dieser Teilklasse aus? Wieviele Objekte gibt es in der Teilklasse? Und: Wie verändern sich die Antworten auf die ersten beiden Fragen, wenn sich x verändert? Die vorliegende Dissertation behandelt Phasenübergänge im Evolutionsprozeß teilweiser Ordnungen und bestimmt die Anzahl teilweiser Ordnungen mit einer gegebenen Anzahl vergleichbarer Paare. Wir bezeichnen durch Pn,d die Klasse aller teilweisen Ordnungen mit n Punkten und dn2 vergleichbaren Paaren. 1978 bestimmte Dhar |Pn,d| im Intervall 1/8 < d < 3/16 und zeigte, daß hier eine typische Ordnung aus drei "Ebenen" besteht. 1979 bestimmten Kleitman und Rothschild |Pn,d| im Intervall 0 < d < 1/8 und zeigten, daß hier eine typische Ordnung aus zwei Ebenen besteht, also bipartit ist. Das Hauptergebnis der Dissertation ist es, ein vollständiges Bild des Evolutionsprozesses zu geben. Wir bestimmen |Pn,d| im gesamten Intervall 0 < d < 1/2 und zeigen, daß es unendlich viele Phasenübergänge gibt. Abschließend beschreiben wir, wie sich die Struktur einer typischen Ordnung während dieser Phasen verändert. / The evolution process of a random structure from a certain class denotes the following "experiment". Choose a parameter of the objects in the class under consideration and consider only the subclass of those objects where the parameter is equal to a fixed value x. Then the following questions arise quite naturally: What does a typical object from this subclass look like? How many objects are there in this subclass? And how do the answers to the first two questions change when x changes? This thesis investigates the phase transitions in the evolution of partially ordered sets and determines the number of partially ordered sets with a given number of comparable pairs. Denote by Pn,d the class of all n-point posets with dn2 comparable pairs. In 1978, Dhar determined |Pn,d| in the range 1/8 < d < 3/16 and showed that here a typical poset consists of three layers. In 1979, Kleitman and Rothschild determined |Pn,d| in the range 0 < d < 1/8 and showed that here a typical poset consists of two layers, i.e. it is bipartite. The main result of this thesis is to complete the picture by describing the whole evolution process of Pn,d in the range 0 < d < 1/2. We determine |Pn,d| for any d and show that there exist an infinite number of phase transitions. Finally we describe how the structure of a typical partially ordered set changes during these phases.

Das Lernen aus strukturierten Eingabe- und Ausgabebeispielen ist die Grundlage für die automatisierte Verarbeitung natürlich auftretender Problemstellungen und eine Herausforderung für das Maschinelle Lernen. Die Einordnung von Objekten in eine Klassentaxonomie, die Eigennamenerkennung und das Parsen natürlicher Sprache sind mögliche Anwendungen. Klassische Verfahren scheitern an der komplexen Natur der Daten, da sie die multiplen Abhängigkeiten und Strukturen nicht erfassen können. Zudem ist die Erhebung von klassifizierten Beispielen in strukturierten Anwendungsgebieten aufwändig und ressourcenintensiv, während unklassifizierte Beispiele günstig und frei verfügbar sind. Diese Arbeit thematisiert halbüberwachte, diskriminative Vorhersagemodelle für strukturierte Daten. Ausgehend von klassischen halbüberwachten Verfahren werden die zugrundeliegenden analytischen Techniken und Algorithmen auf das Lernen mit strukturierten Variablen übertragen. Die untersuchten Verfahren basieren auf unterschiedlichen Prinzipien und Annahmen, wie zum Beispiel der Konsensmaximierung mehrerer Hypothesen im Lernen aus mehreren Sichten, oder der räumlichen Struktur der Daten im transduktiven Lernen. Desweiteren wird in einer Fallstudie zur Email-Batcherkennung die räumliche Struktur der Daten ausgenutzt und eine Lösung präsentiert, die der sequenziellen Natur der Daten gerecht wird. Aus den theoretischen Überlegungen werden halbüberwachte, strukturierte Vorhersagemodelle und effiziente Optmierungsstrategien abgeleitet. Die empirische Evaluierung umfasst Klassifikationsprobleme, Eigennamenerkennung und das Parsen natürlicher Sprache. Es zeigt sich, dass die halbüberwachten Methoden in vielen Anwendungen zu signifikant kleineren Fehlerraten führen als vollständig überwachte Baselineverfahren. / Learning mappings between arbitrary structured input and output variables is a fundamental problem in machine learning. It covers many natural learning tasks and challenges the standard model of learning a mapping from independently drawn instances to a small set of labels. Potential applications include classification with a class taxonomy, named entity recognition, and natural language parsing. In these structured domains, labeled training instances are generally expensive to obtain while unlabeled inputs are readily available and inexpensive. This thesis deals with semi-supervised learning of discriminative models for structured output variables. The analytical techniques and algorithms of classical semi-supervised learning are lifted to the structured setting. Several approaches based on different assumptions of the data are presented. Co-learning, for instance, maximizes the agreement among multiple hypotheses while transductive approaches rely on an implicit cluster assumption. Furthermore, in the framework of this dissertation, a case study on email batch detection in message streams is presented. The involved tasks exhibit an inherent cluster structure and the presented solution exploits the streaming nature of the data. The different approaches are developed into semi-supervised structured prediction models and efficient optimization strategies thereof are presented. The novel algorithms generalize state-of-the-art approaches in structural learning such as structural support vector machines. Empirical results show that the semi-supervised algorithms lead to significantly lower error rates than their fully supervised counterparts in many application areas, including multi-class classification, named entity recognition, and natural language parsing.

Edsger W. Dijkstra prägte im Jahr 1974 den Begriff Selbststabilisierung (self-stabilization) in der Informatik. Ein System ist selbststabilisierend, wenn es von jedem denkbaren Zustand aus nach einer endlichen Anzahl von Aktionen ein stabiles Verhalten erreicht. Im Mittelpunkt dieser Arbeit steht der Entwurf selbststabilisierender Algorithmen. Wir stellen eine Petrinetz-basierte Methode zum Entwurf selbststabilisierender Algorithmen vor. Wir validieren unsere Methode an mehreren Fallstudien: Ausgehend von algorithmischen Ideen existierender Algorithmen beschreiben wir jeweils die die schrittweise Entwicklung eines neuen Algorithmus. Dazu gehört ein neuer randomisierter selbststabilisierender Algorithmus zur Leader Election in einem Ring von Prozessoren. Dieser Algorithmus ist abgeleitet aus einem publizierten Algorithmus, von dem wir hier erstmals zeigen, daß er fehlerhaft arbeitet. Wir weisen die Speicherminimalität unseres Algorithmus nach. Ein weiteres Ergebnis ist der erste Algorithmus, der ohne Time-Out-Aktionen selbststabilisierenden Tokenaustausch in asynchronen Systemen realisiert. Petrinetze bilden einen einheitlichen formalen Rahmen für die Modellierung und Verifikation dieser Algorithmen. / In 1974, Edsger W. Dijkstra suggested the notion of self-stabilization. A system is self-stabilizing if regardless of the initial state it eventually reaches a stable behaviour. This thesis focuses on the design of self-stabilizing algorithms. We introduce a new Petri net based method for the design of self-stabilizing algorithms. We validate our method on several case studies. In each of the case studies, our stepwise design starts from an algorithmic idea and leads to a new self-stabilizing algorithm. One of these algorithms is a new randomized self-stabilizing algorithm for leader election in a ring of processors. This algorithm is derived from a published algorithm which we show to be incorrect. We prove that our algorithm is space-minimal. A further result is the first algorithm for token-passing in a asynchronous environment which works without time-out actions. Petri nets form a unique framework for modelling and verification of these algorithms.

Proteininteraktionen sind entscheidend für zelluläre Funktion. Interaktionen reflektieren direkte funktionale Beziehungen zwischen Proteinen. Veränderungen in spezifischen Interaktionsmustern tragen zur Entstehung von Krankheiten bei. In dieser Arbeit werden funktionale und pathologische Aspekte von Proteininteraktionen analysiert, um Funktionen für bisher nicht charakterisierte Proteine vorherzusagen und Proteine mit Krankheitsphänotypen zu assoziieren. Verschiedene Methoden wurden in den letzten Jahren entwickelt, die die funktionalen Eigenschaften von Proteinen untersuchen. Dennoch bleibt ein wesentlicher Teil der Proteine, insbesondere menschliche, uncharakterisiert. Wir haben eine Methode zur Vorhersage von Proteinfunktionen entwickelt, die auf Proteininteraktionsnetzwerken verschiedener Spezies beruht. Dieser Ansatz analysiert funktionale Module, die über evolutionär konservierte Prozesse definiert werden. In diesen Modulen werden Proteinfunktionen gemeinsam über Orthologiebeziehungen und Interaktionspartner vorhergesagt. Die Integration verschiedener funktionaler Ähnlichkeiten ermöglicht die Vorhersage neuer Proteinfunktionen mit hoher Genauigkeit und Abdeckung. Die Aufklärung von Krankheitsmechanismen ist wichtig, um ihre Entstehung zu verstehen und diagnostische und therapeutische Ansätze zu entwickeln. Wir stellen einen Ansatz für die Identifizierung krankheitsrelevanter Genprodukte vor, der auf der Kombination von Proteininteraktionen, Proteinfunktionen und Netzwerkzentralitätsanalyse basiert. Gegeben einer Krankheit, werden krankheitsspezifische Netzwerke durch die Integration von direkt und indirekt interagierender Genprodukte und funktionalen Informationen generiert. Proteine in diesen Netzwerken werden anhand ihrer Zentralität sortiert. Das Einbeziehen indirekter Interaktionen verbessert die Identifizierung von Krankheitsgenen deutlich. Die Verwendung von vorhergesagten Proteinfunktionen verbessert das Ranking von krankheitsrelevanten Proteinen. / Protein interactions are essential to many aspects of cellular function. On the one hand, they reflect direct functional relationships. On the other hand, alterations in protein interactions perturb natural cellular processes and contribute to diseases. In this thesis we analyze both the functional and the pathological aspect of protein interactions to infer novel protein function for uncharacterized proteins and to associate yet uncharacterized proteins with disease phenotypes, respectively. Different experimental and computational approaches have been developed in the past to investigate the basic characteristics of proteins systematically. Yet, a substantial fraction of proteins remains uncharacterized, particularly in human. We present a novel approach to predict protein function from protein interaction networks of multiple species. The key to our method is to study proteins within modules defined by evolutionary conserved processes, combining comparative cross-species genomics with functional linkage in interaction networks. We show that integrating different evidence of functional similarity allows to infer novel functions with high precision and a very good coverage. Elucidating the pathological mechanisms is important for understanding the onset of diseases and for developing diagnostic and therapeutic approaches. We introduce a network-based framework for identifying disease-related gene products by combining protein interaction data and protein function with network centrality analysis. Given a disease, we compile a disease-specific network by integrating directly and indirectly linked gene products using protein interaction and functional information. Proteins in this network are ranked based on their network centrality. We demonstrate that using indirect interactions significantly improves disease gene identification. Predicted functions, in turn, enhance the ranking of disease-relevant proteins.