Eine der größten Herausforderungen in Data Science ist heutzutage, Daten miteinander in Beziehung zu setzen und ähnliche Daten zu finden. Hierzu kann der aus relationalen Datenbanken bekannte Join-Operator eingesetzt werden. Das Konzept der Ähnlichkeit wird häufig durch mengenbasierte Ähnlichkeitsfunktionen gemessen. Um solche Funktionen als Join-Prädikat nutzen zu können, setzt diese Arbeit voraus, dass Records aus Mengen von Tokens bestehen. Die Arbeit fokussiert sich auf den mengenbasierten Ähnlichkeitsjoin, Set Similarity Join (SSJ). Die Datenmenge, die es heute zu verarbeiten gilt, ist groß und wächst weiter. Der SSJ hingegen ist eine rechenintensive Operation. Um ihn auf großen Daten ausführen zu können, sind neue Ansätze notwendig. Diese Arbeit fokussiert sich auf das Mittel der Parallelisierung. Sie leistet folgende drei Beiträge auf dem Gebiet der SSJs. Erstens beschreibt und untersucht die Arbeit den aktuellen Stand paralleler SSJ-Ansätze. Diese Arbeit vergleicht zehn Map-Reduce-basierte Ansätze aus der Literatur sowohl analytisch als auch experimentell. Der größte Schwachpunkt aller Ansätze ist überraschenderweise eine geringe Skalierbarkeit aufgrund zu hoher Datenreplikation und/ oder ungleich verteilter Daten. Keiner der Ansätze kann den SSJ auf großen Daten berechnen. Zweitens macht die Arbeit die verfügbare hohe CPU-Parallelität moderner Rechner für den SSJ nutzbar. Sie stellt einen neuen daten-parallelen multi-threaded SSJ-Ansatz vor. Der vorgestellte Ansatz ermöglicht erhebliche Laufzeit-Beschleunigungen gegenüber der Ausführung auf einem Thread. Drittens stellt die Arbeit einen neuen hoch skalierbaren verteilten SSJ-Ansatz vor. Mit einer kostenbasierten Heuristik und einem daten-unabhängigen Skalierungsmechanismus vermeidet er Daten-Replikation und wiederholte Berechnungen. Der Ansatz beschleunigt die Join-Ausführung signifikant und ermöglicht die Ausführung auf erheblich größeren Datenmengen als bisher betrachtete parallele Ansätze. / One of today's major challenges in data science is to compare and relate data of similar nature. Using the join operation known from relational databases could help solving this problem. Given a collection of records, the join operation finds all pairs of records, which fulfill a user-chosen predicate. Real-world problems could require complex predicates, such as similarity. A common way to measure similarity are set similarity functions. In order to use set similarity functions as predicates, we assume records to be represented by sets of tokens. In this thesis, we focus on the set similarity join (SSJ) operation. The amount of data to be processed today is typically large and grows continually. On the other hand, the SSJ is a compute-intensive operation. To cope with the increasing size of input data, additional means are needed to develop scalable implementations for SSJ. In this thesis, we focus on parallelization. We make the following three major contributions to SSJ. First, we elaborate on the state-of-the-art in parallelizing SSJ. We compare ten MapReduce-based approaches from the literature analytically and experimentally. Their main limit is surprisingly a low scalability due to too high and/or skewed data replication. None of the approaches could compute the join on large datasets. Second, we leverage the abundant CPU parallelism of modern commodity hardware, which has not yet been considered to scale SSJ. We propose a novel data-parallel multi-threaded SSJ. Our approach provides significant speedups compared to single-threaded executions. Third, we propose a novel highly scalable distributed SSJ approach. With a cost-based heuristic and a data-independent scaling mechanism we avoid data replication and recomputation. A heuristic assigns similar shares of compute costs to each node. Our approach significantly scales up the join execution and processes much larger datasets than all parallel approaches designed and implemented so far.

Die thermische Magnetresonanz (ThermalMR) integriert Radiofrequenz (RF)-induzierte Erwärmung, in vivo Temperaturkartierung mittels MR-Thermometrie, anatomische und funktionelle MR-Bildgebung (MRT) und die Option für die x-Kern-MRT in einem einzigen, vielseitig einsetzbaren RF-Applikator. Der Aufbau erlaubt eine gezielte und überwachte Temperaturmodulation und kann somit als Basis für Studien dienen, welche die Klärung grundlegender Fragen bezüglich der molekularen, biochemischen, sowie physiologischen und therapeutischen Auswirkungen der Temperatur in Organismen ermöglichen. In dieser Arbeit wurde ein kostengünstiges, automatisiertes Open-Source-3D-Mehrzweck-Messsystem mit Submillimeter-Genauigkeit implementiert und validiert, um technische Entwicklungen in der thermischen MR wie Antennendesign, Signalgeneratoren, und simulationsbasierte Methoden zu prüfen. Um den Anforderungen eines modernen ThermalMR-Systems gerecht zu werden, wird ein neuer auf einem Phasenregelkreis basierender RF-Signalgenerator für Hyperthermie entwickelt und über dessen Entwurf, Implementierung, Validierung und Anwendung berichtet. Der Signalgenerator ist in der Lage, 32 unabhängige RF-Signale mit präziser Einstellung der Parameter dieser Signale zu erzeugen. Das in dieser Arbeit entwickelte Mehrkanal-RF-Überwachungsmodul ermöglicht das Detektieren von Abweichungen bezogen auf die gewählten Einstellungen und ermöglicht eine Korrektur der RF-Signale in einem Regelkreis. Darüber hinaus ermöglicht das Überwachungsmodul das Erkennen von Bewegungen und ermöglicht zusätzliche Sicherheit in einem realen Behandlungssetup. In dieser Arbeit wurden Forschung und Entwicklung in Informatik, Physik und Biowissenschaften synergetisch miteinander verbunden. Die in dieser Arbeit entwickelte Infrastruktur bildet eine technologische Basis für zukünftige ThermalMR-Anwendungen. / Thermal magnetic resonance (ThermalMR) integrates radio frequency (RF)-induced heating, in vivo temperature mapping using MR thermometry, anatomic and functional MR imaging (MRI), and the option for x-nuclei MRI in a single, multi-purpose RF applicator. This permits supervised targeted temperature modulation, thus enables pioneering studies to clarify fundamental questions pertaining to the molecular, biochemical, broader physiological and therapeutic effects of temperature in organisms. In this work, a cost-effective, automated open source 3D multipurpose measurement system with submillimeter fidelity was implemented and validated to facilitate technical developments in ThermalMR such as RF antenna design and algorithm verification. The design, implementation, validation, and application of the first phase-locked loop based RF signal generator in hyperthermia that is capable of generating 32 channels of independent RF signals with fine-tuning resolutions of the signals’ parameters meet the demanding requirements of a state-of-the-art RF heating system. The multi-channel RF supervision module developed in this work outperforms state-of-the-art counterparts. The detection of head motion in a hyperthermia setting was demonstrated for the first time with the RF supervision module. This work synergistically connects research and development in computer science, physics, and life science. The infrastructure developed in this work forms a technological basis for future ThermalMR applications.

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.

Alle Lehrkräfte benötigen für ihre Profession spezifische digitale Kompetenzen, um das Potenzial digitaler Medien zum Lehren und Lernen nutzen zu können und um Schüler:innen zu befähigen, kompetent mit digitalen Medien umzugehen. Es fehlt an wirksamen Fortbildungsangeboten. Diese Dissertation möchte einen Beitrag dazu leisten und geht zwei Forschungsfragen nach: 1) Wie sollte eine fächerübergreifende Fortbildung für Lehrkräfte weiterführender Schulen inhaltlich, methodisch-didaktisch und organisatorisch gestaltet sein, um die professionsspezifische digitale Kompetenz der Teilnehmenden für sie zufriedenstellend zu fördern? 2) Welche Wirkung hat die konzipierte Fortbildung auf die selbsteingeschätzte digitale Kompetenz und das berichtete berufliche Handeln mit digitalen Medien? Die theoretische Grundlage für die Konzeption der Fortbildungsreihe bilden der Europäische DigCompEdu-Rahmen und der aktuelle Forschungsstand zu wirksamen Lehrkräftefortbildungen. Als forschungsmethodische Grundlage wurde der iterative Design-Based Research Ansatz gewählt. Das zu Beginn theoriegeleitet entwickelte Fortbildungskonzept wurde mit Hilfe qualitativer und quantitativer Methoden in drei Zyklen mit insgesamt 13 Fortbildungsgruppen und 247 Teilnehmenden weiterentwickelt und evaluiert. Aus der Studie resultierte ein für die Mehrheit zufriedenstellendes und evidenzbasiertes Konzept einer vierteiligen Fortbildungsreihe mit umfassenden Materialien, welches die selbsteingeschätzte digitale Kompetenz signifikant verbessert und das berichtete berufliche Handeln mit digitalen Medien nachweislich verändert. Ferner konnten die aus der Literatur identifizierten Merkmale zur inhaltlichen, methodisch-didaktischen und organisatorischen Gestaltung wirksamer Lehrkräftefortbildungen für diesen Kontext bestätigt, konkretisiert und ergänzt werden, woraus Gestaltungsempfehlungen für zukünftige Lehrkräftefortbildungen zur Förderung der professionspezifischen digitalen Kompetenz abgeleitet werden konnten. / To harness the potential of digital technologies for teaching and learning in schools, and to enable students to use digital technologies competently, teachers need specific digital competencies for their profession. This thesis aims to address the lack in effective Continuous Professional Development (CPD) courses in digital competences by answering the following research questions: 1) How should an interdisciplinary in-service training course for secondary school teachers be designed in terms of content, methodological-didactic and organisational aspects in order to satisfactorily promote the profession-specific digital competence of the participants? 2) What is the impact of the designed CPD course on the self-assessed digital competence of the participants and in their reported professional use of digital technologies? The European Framework DigCompEdu and the state-of-the-art research on effective CPD for teachers form the theoretical basis for the design of the CPD course. The iterative Design-Based Research approach was chosen as the research methodology. The initial theory-based CPD design was continuously re-designed and evaluated in three cycles with a total of 13 groups and 247 participants using qualitative and quantitative methods. The study provided an evidence-based concept for a four-part CPD course that is acceptable to the majority of respondents and that significantly improves the self-assessed digital competence. Furthermore, the design principles identified in the literature for effective CPD in terms of content, methodology, didactics and organisation could be confirmed, specified and extended for the context of the interdisciplinary promotion of DigCompEdu competences of teachers at secondary schools. Finally, recommendations are derived for the design of future CPD courses to promote the digital competences of the profession.

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.

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.

In der Bioinformatik und der Next-Generation Sequenzierung benötigen wir oft große und komplexe Verarbeitungsabläufe um Daten zu analysieren. Die Werkzeuge und Bibliotheken, die hierin die Verarbeitungsschritte bilden, stammen aus unterschiedlichen Quellen und exponieren unterschiedliche Schnittstellen, was ihre Integration in Datenanalyseplattformen erschwert. Hinzu kommt, dass diese Verarbeitungsabläufe meist große Datenmengen prozessieren weshalb Forscher erwarten, dass unabhängige Verarbeitungsschritte parallel laufen. Der Stand der Technik im Feld der wissenschaftlichen Datenverarbeitung für Bioinformatik und Next-Generation Sequenzierung sind wissenschaftliche Workflowsysteme. Ein wissenschaftliches Workflowsystem erlaubt es Forschern Verarbeitungsabläufe als Workflow auszudrücken. Solch ein Workflow erfasst die Datenabhängigkeiten in einem Verarbeitungsablauf, integriert externe Software und erlaubt es unabhängige Verarbeitungsschritte zu erkennen, um sie parallel auszuführen. In dieser Arbeit präsentieren wir Cuneiform, eine Workflowsprache, und ihre verteilte Ausführungsumgebung. Für Cuneiform's Design nehmen wir die Perspektive der Programmiersprachentheorie ein. Wir lassen Methoden der funktionalen Programmierung einfließen um Komposition und Datenabhängigkeiten auszudrücken. Wir nutzen operationelle Semantiken um zu definieren, wann ein Workflow wohlgeformt und konsistent ist und um Reduktion zu erklären. Für das Design der verteilten Ausführungsumgebung nehmen wir die Perspektive der verteilten Systeme ein. Wir nutzen Petri Netze um die Kommunikationsstruktur der im System beteiligten Agenten zu erklären. / Bioinformatics and next-generation sequencing data analyses often form large and complex pipelines. The tools and libraries making up the processing steps in these pipelines come from different sources and have different interfaces which hampers integrating them into data analysis frameworks. Also, these pipelines process large data sets. Thus, users need to parallelize independent processing steps. The state of the art in large-scale scientific data analysis for bioinformatics and next-generation sequencing are scientific workflow systems. A scientific workflow system allows researchers to describe a data analysis pipeline as a scientific workflow which integrates external software, defines the data dependencies forming a data analysis pipeline, and parallelizes independent processing steps. Scientific workflow systems consist of a workflow language providing a user interface, and an execution environment. The workflow language determines how users express workflows, reuse and compose workflow fragments, integrate external software, how the scientific workflow system identifies independent processing steps, and how we derive optimizations from a workflow's structure. The execution environment schedules and runs data processing operations. In this thesis we present Cuneiform, a workflow language, and its distributed execution environment. For Cuneiform's design we take the perspective of programming languages. We adopt methods from functional programming towards composition and expressing data dependencies. We apply operational semantics and type systems to define well-formedness, consistency, and reduction of Cuneiform workflows. For the design of the distributed execution environment we take the perspective of distributed systems. We apply Petri nets to define the communication patterns among the distributed execution environment's agents.

Domänenspezifische Sprachen (DSLs) sind Software-Sprachen, die speziell für bestimmte Anwendungsdomänen entwickelt wurden. Mithilfe von DSLs können Domänenexperten ihr Domänenwissen auf einem hohen Abstraktionsniveau beschreiben. Wie andere Software-Sprachen auch, benötigen DSLs Sprachwerkzeuge, die Assistenz bei der Erstellung und Verarbeitung von domänenspezifischen Modellen bieten. Eine domänenspezifische Werkbank (DSW) ist ein Software-Werkzeug, welches mehrere solcher Sprachwerkzeuge für eine DSL miteinander integriert. Existierende Werkzeuge, die es erlauben eine DSW aufgrund der Beschreibung einer DSL automatisch generieren zu lassen, unterstützen jedoch nicht die Beschreibung und Generierung von editierbaren Sichten. Eine Sicht ist ein Teil einer DSW, der nur einen bestimmten Aspekt eines Modells darstellt. Diese Dissertation stellt spezielle Modelltransformationssprachen (MTLs) vor, mit denen die Synchronisation von Sichten in einer generierten DSW beschrieben werden kann. Dadurch können DSWs mit editierbaren Sichten mittels existierender Werkzeuge zur Generierung von Sprachwerkzeugen erstellt werden. Dafür wird eine DSW für die Nanophysik-Domäne sowie eine Taxonomie von Synchronisationstypen vorgestellt, welche es erlaubt genau zu bestimmen, welche Art von Modelltransformationen für die Synchronisation von Sichten in dieser Werkbank benötigt werden. Entsprechend dieser Anforderungen werden zwei MTLs entwickelt. Insbesondere wird eine bidirektionale MTL entwickelt. Mit solch einer Sprache kann man eine Relation, welche definiert ob zwei Modelle synchron sind, so beschreiben, dass die entsprechende Synchronisationslogik automatisch abgeleitet werden kann. Die gezeigten MTLs werden als interne DSLs - das heißt eingebettet als ausdrucksstarke Bibliotheken - in der Programmiersprache Scala implementiert. Auf diese Weise kann Scalas Typprüfung genutzt werden, um Transformationen und deren Komposition statisch zu verifizieren. / Domain-specific languages (DSLs) are software languages which are tailored to a specific application domain. DSLs enable domain experts to create domain-specific models, that is, high-level descriptions of domain knowledge. As any other software languages, DSLs rely on language tools which provide assistance for processing and managing domain-specific models. A domain-specific workbench is an integrated set of such tools for a DSL. A recently proposed approach is to automatically generate a domain-specific workbench for a DSL from a description of that DSL. However, existing tools which apply this approach do not support to describe and generate editable domain-specific views. A view is a part of domain-specific workbench that presents only one aspect of a model, for example, its hierarchical structure. This dissertation presents special model transformation languages which support the description of view synchronization in a generated domain-specific workbench. This allows a multi-view domain-specific workbench to be created with existing tools for language tool generation. We present a generated domain-specific workbench for the nanophysics domain and present a taxonomy of synchronization types. This allows us to precisely define what model transformations are required for view synchronization in that workbench. According to these requirements, we develop two transformation languages by adapting existing ones. In particular, we develop a bidirectional transformation language. With such a language one can describe a relation which defines whether two models are in sync and let the synchronization logic be inferred automatically. We implement model transformation languages as internal DSLs - that is, embedded as expressive libraries - in the Scala programming language and use Scala''s type checking for static verification of transformations and their composition.