Autor*innen mit den meisten Dokumenten
Auflistung nach:
Neueste Veröffentlichungen
- KonferenzbeitragWerkzeuge und Methoden zum Lösen von Problemen mittels Baumweite(D22, 2022) Hecher, MarkusIn den letzten Jahrzehnten konnte ein beachtlicher Fortschritt im Bereich der Aussagenlogik verzeichnet werden, der sich durch überwältigend schnelle Computerprogramme (Solver) zur Lösung aussagenlogischer Formeln äußert. Einer der Gründe dieser Schnelligkeit befasst sich mit strukturellen Eigenschaften von Probleminstanzen, zum Beispiel der sogenannten Baumweite, wel- che versucht zu messen, wie groß der Abstand von Probleminstanzen zu einfachen Strukturen (Bäumen) ist. Diese Arbeit befasst sich mit Problemen der Künstlichen Intelligenz (KI) sowie Baumweite- basierenden Methoden und Werkzeugen zum Lösen dieser. Wir präsentieren einen neuen Typ von Problemreduktion, den wir als ”zerlegungsangeleitet“ bezeichnen. Dieser ist die Basis, um eine lange offen gebliebene Frage betreffend quantifizierter, aussagenlogischer Formeln (QBF) bei beschränkter Baumweite zu zeigen. Die Lösung der Frage ermöglicht ein neues Meta-Werkzeug zum Beweisen präziser unterer Laufzeitschranken einer Vielzahl von Problemen der KI. Trotz dieser Schranken implementieren wir einen Solver für Erweiterungen von Sat, der Baumweite effizient ausnutzt.
- KonferenzbeitragDrohnennetzwerke zur Suche und Rettung(D22, 2022) Hayat, SamiraDiese Arbeit befasst sich mit dem komplexen Problem des Entwurfs von Drohnennetzwer- ken. Drohnenanwendungen sind sehr vielfältig und können mit traditionellen Netzwerkdesignmethoden nicht erfolgreich bewältigt werden. Alternativ schlagen wir vor, die grundlegenden Fragen für Droh- nennetzwerkanwendungen zu beantworten: Welche Daten müssen übertragen werden? Wie werden die Daten von Punkt A zu Punkt B im Netzwerk übertragen? Wann (zu welchen Zeitpunkten) müssen die Daten übertragen werden? Wir stellen fest, dass Kommunikation in einem Drohnennetzwerk sowohl dem Missionsziel (für die Übertragung von Sensordaten) als auch der Missionsdurchführung (Missionskoordination) dient, weshalb wir eine abstimmbare und modulare Systemarchitektur vorschlagen. Abhängig von den Missionsanforderungen können verschiedene Kommunikations- und Koordinationsmodule hinzugefügt werden, ohne dass das gesamte System geändert werden muss. Die Systemarchitektur wird für einen Such- und Rettungseinsatz implementiert, wobei bestehende Kommunikationstechnologien im Experiment getestet und neuartige Koordinationsalgorithmen vorgeschlagen werden.
- KonferenzbeitragHochqualitativ Verifikation für VP-basierte Heterogene Systeme(D22, 2022) Hassan, MuhammadIn dieser Dissertation werden mehrere neuartige Ansätze entwickelt, die verschiedene Verifikationsaspekte abdecken, um den modernen, auf Virtuellen Prototypen (VP)-basierten, Verifikationsablauf stark zu verbessern. Die Beiträge sind im Wesentlichen in vier Bereiche unterteilt: Der erste Beitrag führt eine neue Verifikationsperspektive für VPs ein, indem er Metamorphic Testing (MT) verwendet, da im Gegensatz zu modernen VP-basierten Verifikationsabläufen keine Referenzmodelle/-werte für die Verifikation benötigt werden. Der zweite Beitrag schlägt hochqualitative Methoden zum Schließen der Code-Abdeckung in modernen VP-basierten Verifikationsabläufen vor, indem er Mutationsanalyse und stärkere Abdeckungsmetriken wie Datenfluss- Abdeckung berücksichtigt. Der dritte Beitrag besteht aus einer Reihe hochqualitativ, neuartiger, systematischer und leichtgewichtigen funktionalen Methoden zur Verbesserung der relevanten Ab- deckungsmetriken. Der vierte und letzte Beitrag dieser Arbeit sind neuartige Ansätze, die eine frühzeitige Sicherheitsvalidierung von VPs ermöglichen. Alle Ansätze werden im Detail vorgestellt und ausführlich mit mehreren Experimenten evaluiert, die ihre Effektivität durch einen hochqualitativ VP-basierten Verifikationsfluss für heterogene Systeme deutlich machen.
- KonferenzbeitragStern-Topologie Entkoppelte Zustandsraumsuche(D22, 2022) Gnad, DanielDie Zustandsraumsuche ist ein weit verbreitetes Konzept in vielen Bereichen der Informatik. Die Größe der zu durchsuchenden Zustandsräume wächst jedoch typischerweise exponentiell mit der Größe einer kompakten, faktorisierten Modellbeschreibung – das ist das bekannte Problem der Zustandsexplosion. Die Entkoppelte Zustandsraumsuche (entkoppelte Suche) beschreibt einen neuartigen Ansatz um der Zustandsexplosion entgegenzuwirken. Hierfür wird die Struktur des Modells, insbesondere die bedingte Unabhängigkeit von Systemkomponenten in einer Sterntopologie, ausgenutzt. Diese Unabhängigkeit ergibt sich ganz natürlich bei vielen faktorisierten Modellen deren Zustandsräume aus dem Produkt mehrerer Komponenten bestehen. In der Dissertation wird die ent- koppelte Suche in der Planung – als Teil der Künstlichen Intelligenz (KI) – und in der Verifikation mittels Modellprüfung eingeführt. Das Konzept des entkoppelten Zustandsraums wird auf Basis von etablierten Formalismen entwickelt und seine Korrektheit bezüglich der exakten Erfassung der Erreichbarkeit von Modellzuständen bewiesen. Damit kann die entkoppelte Suche mit beliebigen Suchalgorithmen genutzt und mit komplementären Techniken kombiniert werden. In der Dissertation wird gezeigt dass die entkoppelte Suche den Suchaufwand exponentiell stärker reduzieren kann als existierende alternative Ansätze, insbesondere die Reduktion partieller Ordnung, Symmetriereduktion, Entfaltung von Petri-Netzen und symbolische Suche. Empirisch kann die entkoppelte Suche sowohl in der Planung als auch in der Modellprüfung etablierte Systeme deutlich übertreffen.
- KonferenzbeitragSelbstadaptive Fitness in evolutionären Prozessen(D22, 2022) Gabor, ThomasEvolutionäre Prozesse modellieren die Entwicklung von Objekten mit zunächst zufälligen Eigenschaften zu Objekten, deren Eigenschaften einer Ordnung oder einem bestimmten Ziel (genannt Fitness) folgen. Evolutionäre Prozesse treten in Software häufig als Optimierungsalgorithmen oder beim maschinellen Lernen auf, wobei ihr Ziel meist extrinsisch durch einen Designer oder Programmierer bestimmt ist. Oft ist es jedoch von Vorteil, wenn besagte Algorithmen ihre Fitnessberechnung während ihrer Ausführung intrinsisch selbst adaptieren können. Wir verfolgen dieses Phänomen zurück auf künstliche Chemiesysteme (artificial chemistry systems), wo Fitness ohne Designer entsteht. Wir untersuchen diversitätsbasierte Fitnessfunktionen in evolutionären Algorithmen und können erstmalig ihre Effektivität begründen, indem wir das theoretische Modell der produktiven Fitness definieren. Schließlich finden wir einen Effektivitätsgewinn auch beim Zusammenspiel von evolutionären Algorithmen und bestärkendem Lernen (reinforcement learning), wobei beide Methoden allein durch eine wechselseitig adaptive Fitness interagieren. Dieses Konzept lässt sich auch als Architekturmuster für Softwaresysteme verallgemeinern.
- KonferenzbeitragProgrammaggregation mit algebraischen Entscheidungsdiagrammen(D22, 2022) Gossen, Frederik JakobIm Rahmen dieser Dissertation wurde das Potential von algebraischen Entscheidungsdiagrammen (ADDs) als Programmrepräsentation für deren Optimierung untersucht. Dabei wurden domänenspezifische Sprachen, maschinell erlernte Modelle und allgemeine Programmiersprachen betrachtet. Insbesondere die Anwendung auf Random Forests, eine Methode des klassischen maschinellen Lernens, war besonders erfolgreich. Hier konnten nicht nur Beschleunigungen von mehreren Größenordnungen erreicht werden, sondern auch gleich drei wichtige Erklärbarkeitsprobleme gelöst werden. Random Forests, die als nicht interpretierbare Black-Box-Modelle angesehen werden, könen so semantisch aggregiert und verständlicher dargestellt werden. Das Resultat der Ag- gregation kann als semantisch äquivalentes White-Box-Modell angesehen werden. Die Lösung der Erklärbarkeitsprobleme ist beispielsweise in der Medizin oder im Bankensektor von enormer Bedeutung. Hier müssen automatisierte Entscheidungen immer erklärbar sein.
- Konferenzbeitrag
- KonferenzbeitragTrace-basierte Erkennung und Analyse von Speicheranomalien(D22, 2022) Weninger, MarkusModerne Programmiersprachen nutzen automatische Speicherbereinigung, um fehleranfällige manuelle Speicherverwaltung zu vermeiden. Dennoch können Anomalien wie Speicherlecks auftreten, die sich drastisch auf die Leistung einer Anwendung auswirken und sogar Abstürze herbeiführen können. Die meisten modernen Werkzeuge nutzen für ihre Speicheranalysen jedoch leider nur Speicherauszüge, d.h. sie inspizieren den Speicher nur an einem oder wenigen bestimmten Zeitpunkten. Diese bieten aber oft nicht genug Details, um zur Ursache des Problems vorzudringen. Unser Ansatz nutzt daher Traces, kontinuierliche Aufnahmen von Ereignissen wie beispielsweise Allokationen oder Speicherbereinigungsoperationen. Diese Arbeit zeigt, wie Traces genutzt werden können, um die (automatische) Speicherproblemerkennung und -analyse zu verbessern. Sie schlägt unter anderem Algorithmen zur Aufzeichnungsverarbeitung vor und führt neuartige Anomalieanalysen (z.B. die automatisierte Analyse des Wachstums von Datenstrukturen) sowie interaktive Visualisierungstechniken ein. Ferner untersucht sie, wie (unerfahrene) Benutzer sich bei der Speicheranalyse verhalten und wie Werkzeuge verbessert werden können, um diese Nutzer besser zu unterstützen und anzuleiten.
- KonferenzbeitragGenerative Modelle für pathologische Bilddaten(D22, 2022) Uzunova, HristinaDeep-learning-basierte Algorithmen haben sich im Bereich der medizinischen Bildverarbeitung als besonders geeignet erwiesen, allerdings benötigen diese eine große Trainingsdatenmengen mit gegebenen Expertenannotationen. Die Erstellung solcher annotierter Datensätze für Bilddaten mit vorhandenen pathologischen Strukturen gilt als besonders herausfordernd, da die Variabilität der Pathologien verglichen mit normalen anatomischen Strukturen enorm ist. In dieser Arbeit werden deep-learning-basierte generative Modelle eingesetzt und weiterentwickelt, um die Herausforderungen von pathologischen Strukturen zu bewältigen. Einerseits wird ein variationeller Autoenocoder für die unüberwachte Detektion von Pathologien eingesetzt, andererseits werden Ansätze basierend auf GANs (generative adversarial networks) entwickelt, um realistische künstliche annotierte Bilder mit pathologischen Strukturen zu generieren. Weiterhin können die vorgestellten Ansätze für die Verbesserung der Bildregistrierung und Segmentierung von Bildern mit Pathologien eingesetzt werden.
- KonferenzbeitragSkalierbare und vertraulichkeitswahrende Off-Chain Berechnungen(D22, 2022) Eberhardt, JacobBlockchains erlauben sich gegenseitig mistrauenden Parteien gemeinsame Transaktionen auszuführen und deren Historie unveränderlich zu speichern. Aufgrund ihres technischen Aufbaus leiden Blockchains jedoch unter niedrigem Durchsatz, fehlender Skalierbarkeit und schwachen Datenschutzgarantien. Diese Arbeit adressiert diese Probleme durch das neuartige Konzept des Off- Chainings: Daten und Berechnungen werden von einer Blockchain auf externe Resourcen ausgelagert - jedoch ohne dabei Schlüsseleigenschaften der Blockchain zu komprommittieren. Insbesondere verifizierbare Off-Chain Berechnungen stellen ein mächtiges Werkzeug zur Erhöhung des Durchsatzes und der Gewährleistung von Vertraulichkeit dar. Allerdings fehlen geignete Realisierungsansätze. Unsere Analyse des Designraums identifiziert zk-SNARKs, eine Klasse nicht-interaktiver Protokolle für kryptographische Zero-Knowledge Beweise, als vielversprechenden Ansatz. Allerdings ist die Instanziierung dieser Protokolle komplex und somit wenigen Experten vorbehalten. Geeignete Pro- grammierabstraktionen und softwaretechnische Werkzeuge fehlen. Um dieses Problem zu adressieren, präsentieren wir ZoKrates, die erste höhere Programmiersprache und Sammlung von Softwarewerkzeu- gen zur Übersetzung und Ausführung zk-SNARK-basierter verifizierbarer Off-Chain Berechnungen. Wir demonstrieren Relevanz und Anwendbarkeit an drei dezentralen Applikationen: Peer-to-Peer Energiehandel, Blockchain-Relays und anonyme Token-Transfers. Die im Kontext dieser Arbeit entstandenen Softwarelösungen finden darüber hinaus unabhängige Anwendung in Wissenschaft und Industrie.