Hybride Systeme

Studentische Arbeiten

Allgemeines

Auf dieser Seite finden Sie einen Ausschnitt aus den möglichen Themenbereichen, die sowohl für studentische Abschlussarbeiten (Individuelles Projekt, Diplomarbeit, BSc-/MSc-Abschlussarbeiten) infrage kommen können, als auch im Rahmen einer Mitarbeit als studentische / wissenschaftliche Hilfskraft geeignet sind. Bitte verstehen Sie diese Liste nicht als vollständige Aufzählung. Wir sind gerne bereit, im persönlichen Gespräch eine Themenfindung im gemeinsamen Interessengebiet durchzuführen.

Wir haben zur Zeit mehrere offene Stellen für studentische / wissenschaftliche Hilfskräfte. Wenn Sie engagiert und an aktuellen Forschungsfragen in einem unserer Themenfelder interessiert sind, sprechen Sie uns bitte an!

Themen

Parallel-Implementierung eines Statistischen Model Checking Verfahrens

Moderne Systeme werden aufgrund von voranschreitender Automation immer komplexer und gleichzeitig haben sie eine größere Abhängigkeit von ihrer Umwelt. So müssen z.B. hochautomatisierte Fahrfunktionen in neueren Autos ihre Umwelt genau wahrnehmen - z.B. die Position des vorherfahrenden Fahrzeuges bestimmen und auf diese adäquat reagieren. Aufgrund der Variabilitäten, welche in der Umwelt auftreten können, ist ein Sicherheitsnachweis, also dass das Fahrzeug / das Assistenzsystem seine Funktion sicher ausführt nur schwer zu erbringen.

Eine mögliche Option ist es, auf Simulationen zurückzugreifen, welche mehrere verschiedene Umweltsituationen virtuell simulieren und jeweils die Güte bzw. die Sicherheit innerhalb des Simulationslaufes bewerten. Eine Absicherung des Gesamtsystems ist somit aber nicht mehr formal vollständig möglich, sondern ist von statistischer Natur.

Ziel der Arbeit soll es sein, zu analysieren, ob der Bias einer parallelen Implementierung eines statistical model checking Verfahrens behoben werden kann. Eine genauere Beschreibung des zugrunde liegenden Verfahrens sowie mögliche Teilaufgaben finden sich in folgendem PDF.

Entwicklung einer Fallstudie zu "discounted measures"

Die meisten Telefongespräche dauern eher kurz, wenige wirklich lang. Ohne einen Prozentsatz nennen zu wollen, dauert sicherlich ein nur verschwindend geringer Teil mehr als ein paar Stunden. Wenn nun jemand eine Telefonanlage baut und ihre Güte abschätzen will, so müssen von diversen beteiligten Komponenten die jeweiligen Ausfallwahrscheinlichkeiten herangezogen werden, Fehlerfortpflanzungen berücksichtigt und Redundanzen genau verstanden werden. Daneben aber spielt die – sicher für einen Telefonanlagenhersteller wesentlich genauer quantifizierbare – Intuition, dass ein Ausfall, der nur bei sehr langer Gesprächsdauer wahrscheinlich ist, wesentlich seltener in der Praxis vorkommen wird als einer, der schon nach wenigen Sekunden eine signifikante Wahrscheinlichkeit aufweist, eine wichtige Rolle, um zu einem relevanten Gütemaß zu kommen.

Ebenfalls im Sonderforschungsbereich AVACS arbeiten wir am Bau von Solvern für probabilistische hybride Systeme. Diese weisen neben dem Zusammenspiel von diskretem und kontinuierlichem Verhalten auch Übergangswahrscheinlichkeiten an den Transitionen auf. Für den Solver SiSAT soll im Rahmen dieses Themas eine Fallstudie entwickelt werden, bei der die oben genannte Intuition, dass die Verteilung der typischen Benutzungen eines Systems eine Rolle spielen kann, besonders deutlich wird. Zunächst würde es dabei um die Identifikation eines realistischen Systems mit geeigneten Eigenschaften gehen. Anschließend dann um die Abstraktion von irrelevanten Systemgrößen und damit um die Modellierung dieses Systems in der Eingabesprache von SiSAT. Schließlich soll mit Hilfe der Fallstudie die Unterstützung von SiSAT für die oben intuitiv beschriebenen "discounted measures" evaluiert werden.

Entwicklung eines lernenden stochastischen SAT-Solvers

Das stochastische SAT-Problem oder SSAT-Problem ist eine Erweiterung des Erfüllbarkeitsproblems der Aussagenlogik, das auch als SAT-Problem bekannt ist. Während das SAT-Problem "nur" danach fragt, ob eine gegebene Boolesche Formel eine Lösung besitzt oder nicht, verlangt das SSAT-Problem erheblich mehr: Wir wollen wissen, ob die Gesamtheit aller Lösungen einer gegebenen Formel eine gewisse Wahrscheinlichkeitsmasse überschreitet oder nicht.

Obwohl oder gerade weil SSAT ein schwieriges Problem ist, und zwar sowohl theoretisch als auch praktisch, hat es viele praktische Anwendungen, beispielsweise im Lösen von probabilistischen Planungsproblemen oder in der Modelprüfung von probabilistischen Automaten. Diese Anwendungen, vor allem im industriellen Kontext, erfordern praktisch effiziente Verfahren zum Lösen von SSAT-Problemen. In den letzten Jahren wurde eine Reihe solcher so genannter SSAT-Solver mit immer steigender Effizienz veröffentlicht.

Dieses Thema beschäftigt sich mit einer vielversprechenden algorithmischen Optimierung von SSAT-Solvern, dem sogenannten "Lernen von Klauseln". Dieses Verfahren wird bereits seit langem sehr erfolgreich in SAT-Solvern eingesetzt. Die grobe Idee dieser Optimierung ist es, während der Suche nach einer Lösung einer Booleschen Formel neues Wissen logisch herzuleiten und für die weitere Suche auszunutzen. Leider war ein ähnliches Verfahren für SSAT-Solver bislang unbekannt. Jedoch wurden vor kurzem die theoretischen Grundlagen eines Lernverfahrens für SSAT gelegt. Letzteres beruht auf einer Verallgemeinerung des Resolutionskalküls für SAT.

Das "Lernen von Klauseln" steigert zudem die Effizienz zweier weiterer Optimierungen, die ebenfalls aus dem SAT-Bereich bekannt sind und die Lösungssuche beschleunigen: "Backjumping" und "Unit Propagation". Grob gesagt, versuchen diese Verfahren mit Hilfe des Wissens aus den gelernten Klauseln, Teile des möglichen Lösungsraumes einfach auszulassen.

Die Bearbeitung dieses Themas beinhaltet folgende Punkte

  • Einarbeitung in SSAT und deren Lösungsverfahren
  • Einarbeitung in das Resolutionskalkül für SSAT
  • Erarbeitung von Ideen zum Einsatz des Klausellernens, Backjumping und Unit Propagation in SSAT-Solver unter besonderer Berücksichtigung effizienter Datenstrukturen
  • Implementierung eines SSAT-Solvers und oben genannter Optimierungen
  • Empirische Untersuchung der Neuerungen

Zur Bearbeitung des Themas werden keine besonderen theoretischen Vorkenntnisse erwartet. Grundlegende Kenntnisse über SAT oder angrenzende Themen wären vorteilhaft. Aufgrund des Implementierungsteils wird allerdings davon ausgegangen, das Grundkenntnisse im Umgang mit einer Programmiersprache vorhanden sind.

Entwicklung einer Eingabesprache für Splitting-Heuristiken

Einer der Kernbestandteile eines intervallbasierten Solvers sind so genannte Splitting-Heuristiken, die auswählen, welche Variable als nächstes eine Entscheidung erfahren soll und wie diese Entscheidung aussieht. So könnte eine solche Heuristik beispielsweise sein, zunächst alle booleschen Variablen zu "splitten", d.h. sich jeweils zu entscheiden, welche true und welche false sein sollen, und anschließend die Intervalle für die reellwertigen Variablen zu spalten. Dabei kann es also Gruppen von Variablen geben, die sich implizit (zum Beispiel aus dem Variablentyp) ergeben oder die explizit (zum Beispiel durch Tags im Eingabeformat) gesetzt werden. Innerhalb dieser Gruppen kann es dann bestimmte Regeln geben, in welcher Reihenfolge die Variablen gesplittet werden sollen (zum Beispiel fest vorgegeben oder dynamisch nach "Aktivität" der Variablen in vom Solver gefundenen Konflikten).

Zur Zeit müssen derartige Heuristiken von Hand ausprogrammiert und an der entsprechenden Stelle im Solver eingefügt werden. Um leichter Experimente mit komplexen Splitting-Heuristiken durchführen zu können, wäre es hingegen hilfreich, eine Art Interpreter zur Verfügung zu haben, der – aufbauend auf ein paar atomaren Operationen – verschiedene konkrete Heuristiken ausführen kann, die in einer zu entwickelnden Eingabesprache formuliert werden können. Zu Ihrer Aufgabe könnte also gehören, eine vorgegebene Menge von atomaren Operationen abzurunden und eine dazu passende erweiterbare Syntax für eine Strategie-Sprache zu entwickeln, einen Parser dafür zu bauen und einen Interpreter für die Zwischendarstellung, der Zugriff auf die vorhandenen Solver-Methoden nimmt, um die Strategie auszuführen.

Die Arbeit ist hervorragend als HiWi-Tätigkeit geeignet, da viele Vorüberlegungen vorhanden sind, die unter Anleitung umgesetzt werden könnten. Gleichzeitig könnte sie aber auch als Abschlussarbeit ausgestaltet werden, wobei dann ein zusätzlicher Fokus auf die eigentlichen Splitting-Heuristiken gelegt würde, und eine Evaluationsphase hinzu käme, bei der verschiedene Heuristiken gegeneinander experimentell verglichen werden müssten.

Vergleich verschiedener Solver

Um ein genaueres Bild von der Leistungsfähigkeit unterschiedlicher Solver auf einer gemeinsamen Klasse von Problemen zu gewinnen, würden Sie bei Bearbeitung dieses Themas zunächst geeignete Fallstudien identifizieren, die sich für von uns vorgegebene Solver kodieren lassen. Sie würden dann Vergleiche bei der Laufzeit und anderer relevanter Messgrößen durchführen und versuchen, durch Modifikation der Modelle herauszufinden, ob sich bestimmte Gesetzmäßigkeiten herausfinden lassen (bspw. eine Korrelation zwischen einer leicht messbaren Eigenschaft eines Modells und einem zu erwartenden Vorteil des einen oder anderen Solvers auf diesem Modell).

Interesse?

Sollten Sie an einem der oben genannten Themen Interesse haben oder sich vorstellen können, an einem vergleichbaren Thema zu arbeiten, sprechen Sie uns bitte an.