http://dl.gi.de/handle/20.500.12116/24 2026-07-21T13:03:07Z 2026-07-21T13:03:07Z Hecher, Markus http://dl.gi.de/handle/20.500.12116/39862 2022-12-02T12:57:55Z 2022-01-01T00:00:00Z

Werkzeuge und Methoden zum Lösen von Problemen mittels Baumweite . Hecher, Markus Hölldobler, Steffen In 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.

2022-01-01T00:00:00Z Hayat, Samira http://dl.gi.de/handle/20.500.12116/39861 2022-12-02T12:57:55Z 2022-01-01T00:00:00Z

Drohnennetzwerke zur Suche und Rettung Hayat, Samira Hölldobler, Steffen Diese 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.

2022-01-01T00:00:00Z Hassan, Muhammad http://dl.gi.de/handle/20.500.12116/39860 2022-12-02T12:57:55Z 2022-01-01T00:00:00Z

Hochqualitativ Verifikation für VP-basierte Heterogene Systeme Hassan, Muhammad Hölldobler, Steffen In 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.

2022-01-01T00:00:00Z Gnad, Daniel http://dl.gi.de/handle/20.500.12116/39858 2022-12-02T12:57:54Z 2022-01-01T00:00:00Z

Stern-Topologie Entkoppelte Zustandsraumsuche Gnad, Daniel Hölldobler, Steffen Die 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.

2022-01-01T00:00:00Z