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 Interessensgebiet 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

Entwicklung eines graphischen und textuellen Automaten-Frontends

In unserer Abteilung werden zusammen mit Kollegen aus dem Sonderforschungsbereich AVACS Solver für verschiedene Klassen von Constraint-Systemen entwickelt (zum Beispiel HySAT und iSAT). Die Eingabesprachen dieser Werkzeuge erlauben die prädikative Modellierung hybrider Systeme mit Hilfe boolescher Kombinationen von arithmetischen Ausdrücken. Daneben kann man in diesen Sprachen jedoch auch vieles andere ausdrücken, was sich deklarativ beschreiben lässt, zum Beispiel würde man sich die Lösungen für

DECL
    float [-10, 10] x, y;
EXPR
    x = sin(y) and y = sin(x);

berechnen lassen können. So allgemeine Problembeschreibungen dadurch auf der einen Seite zugelassen werden, so schwierig kann es auf der anderen Seite sein, "gute" Modelle hybrider Systeme zu finden. Vieles, was intuitiv einfach aussieht, ist für den Solver letztlich schwer zu lösen.

In diesem Kontext würden wir gerne zunächst eine textuelle Beschreibungssprache und später darauf aufbauend eine graphische Automatensprache entwickeln, die es erlaubt, Modelle intuitiv aufzuschreiben und gleichzeitig aber von der später zu nutzenden prädikativen Solver-Eingabesprache zu abstrahieren. Dabei sollen verschiedene Übersetzungschemata von der Automaten- in die Logikwelt implementiert werden, so dass die fehleranfällige manuelle Übersetzung entfallen kann und trotzdem verschiedene Beschreibungen desselben Automaten ausprobiert werden können.

Im Rahmen einer HiWi-Tätigkeit würde Ihr Fokus auf der Unterstützung bei der Implementierung und der Evaluation liegen, oder je nach eigenem Interesse natürlich auch gerne mit größerer Eigenständigkeit in den anderen sich ergebenden Fragestellungen. Im Rahmen einer Abschlussarbeit würden wir von Ihnen erwarten, dass sie das Thema auf jeden Fall selbstständig bearbeiten und unsere Rolle würde dementsprechend stärker beratend sein. Der Zuschnitt der Arbeit würde natürlich der jeweiligen Art der Abschlussarbeit angepasst werden und Schwerpunkte gemeinsam ausgewählt werden.

Verwendung von Potentialfeldern zur Fahrzeugsteuerung

Bei der Fahrt eines Fahrzeuges von einem Startpunkt zu einem Zielpunkt ist die Erkennung und Untersuchung der zugrundeliegenden Mechanismen, die bei einer solchen Fahrt auftreten und den Ablauf der Fahrt bestimmen, von hoher Relevanz. Insbesondere stellt sich die Frage auf welcher Basis und unter welchen Einflüssen der Lenker des Fahrzeuges seine Entscheidungen trifft um die Strecke abzufahren.

Ein möglicher Ansatz zur Beantwortung dieser Frage bietet die Verwendung eines verformbaren Potentialfeldes, dass sich zusammen mit Fahrzeug und Fahrer bewegt, die in diesem positioniert sind. Das Feld beschreibt hierbei die Bewegungsmöglichkeiten des Fahrzeuges und erlaubt somit beispielsweise Aussagen über sicheres Reisen. Die Faktoren, die zu einer Verformung des Feldes führen und somit auch die Bewegungsmöglichkeiten einschränken bzw. aufweiten sind im einfachsten Fall unbewegte und bewegte Hindernisse, die das Feld passiv beschränken oder aktiv eindrücken. Eine weiterführende Annäherung würde beispielsweise die Wirkung von Verkehrszeichen, die beispielsweise Bewegungsmöglichkeiten einschränken, obwohl kein physikalisches Hindernis vorhanden ist, oder auch natürliche Gegebenheiten wie Dunkelheit oder Nebel betrachten.

In dieser Bachelorarbeit machen Sie sich zunächst mit der vorhandenen Literatur vertraut. In einem zweiten Schritt finden Sie einen Weg Fahrverhalten auf der Basis von Potentialfeldern in Form eines Modells zu implementieren, welches innerhalb einer geeigneten Simulationsumgebung (bspw. TORCS) agieren kann.

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.

Bau eines Satisfiability modulo theories (SMT) Solvers auf einer Grafikkarte (GPGPU)

Moderne GPUs (Graphical Processing Units) sind Meister der parallelen Abarbeitung von Programmen. Diese spezialisierte Rechenleistung, die ursprünglich für die Darstellung dreidimensionaler Grafiken entwickelt wurde, wird in jüngerer Zeit immer stärker auch allgemeinen (general purpose) Rechenaufgaben gegenüber geöffnet. Typischerweise sind es Simulationen, bei denen nur wenige verschiedene Operationen auf einer großen Menge an Daten angewandt werden müssen, die besonders von einer Portierung auf derartige GPGPUs profitieren können.

Im Rahmen dieses Themas würden Sie sich zunächst in die GPGPU-Programmierung einarbeiten. Ferner würden Sie einen isolierten Kern der existierenden Solver-Algorithmik von iSAT auf Parallelisierbarkeit untersuchen und gegebenenfalls modifizierte Ansätze vorschlagen, die besser zur gewählten Architektur passen würden. Auf dieser Grundlage wäre dann von Ihnen Implementierungsarbeit zu leisten und durch Experimente eine Evaluation durchzuführen. Die Arbeit lässt sich durch Weglassen einiger wünschenswerter Eigenschaften des dabei entstehenden Solvers an die verschiedenen Anforderungen der unterschiedlichen Typen von Abschlussarbeiten anpassen.

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.