Minimierung von nicht-deterministischen Büchi-Automaten mit Propositionen
Abstract - Zusammenfassung
Es soll die Minimierung für nicht-deterministische Büchi-Automaten so angepasst werden, dass die Eingabewerte der Transitionen durch boolesche Kombinationen aus Propositionen beschrieben werden können, anstatt konkret angegeben werden zu müssen.
Problem Statement - Beschreibung
Wenn ein Monitor für eine Formel der Linear Temporal Logic (LTL) generiert wird, um diesen unter Anderem für Runtime-Verification zu nutzen, entstehen dabei in den Automaten, die als Zwischenschritte konstruiert werden, sehr viele Transitionen. Der Grund dafür ist, dass das Alphabet für eine LTL-Formel die Potenzmenge der Menge der Propositionen ist und jedes Element des Alphabetes von jedem Zustand eines Automaten aus als Eingabe für eine Transition auftreten kann. Um diese große Menge an Transitionen zu verkleinern und dadurch Zeit bei der Monitorgenerierung zu sparen, sollen nun die Eingabesymbole von Transitionen als boolesche Kombination aus Propositionen beschrieben werden. Das obere Bild zeigt den NBA, wie er aktuell aussieht und das untere Bild zeigt, wie er aussehen soll. Dabei werden zum Beispiel die Transitionen von q1 nach q1 im oberen Automaten durch die eine Transition im unteren Automaten beschrieben, wobei die Eingabesymbole der Transitionen des oberen Automaten genau alle Modelle für die Eingabeformel der Transition des unteren Automaten sind.
Alle Schritte der Monitorgenerierung für LTL-Formeln können mit booleschen Kombinationen aus Propositionen an den Kanten wie vorher durchgeführt werden, bis auf die Minimierung der NBAs. Die aktuell genutzte Minimierung für NBAs wird in [1] beschrieben und soll entsprechend angepasst werden.
Die Monitorgenerierung für LTL-Formeln wurde in der Logik- und Automatenbibliothek RltlConv umgesetzt. Aktuell wird in RltlConv für die Minimierung von NBAs eine NBA-Minimierungsbibliothek benutzt, die auf [1] basiert. Die in dieser Arbeit entwickelte Minimierung soll dann in Scala in RltlConv implementiert werden und die bisher genutzte Bibliothek ersetzen.
Goals - Ziele
- Anpassen der Minimierung für NBAs, damit boolesche Kombinationen als Eingaben für Transitionen genutzt werden können
- Implementieren der neuen Minimierung in RltlConv in Scala
Workplan - Vorgehen
- Mit NBAs vertraut machen
- Mit der Minimierung aus [1] vertraut machen
- Die Minimierung entsprechend anpassen
- Mit RltlConv vertraut machen
- Implementieren der neuen Minimierung in Scala
Requirements - Anforderungen
Es sollten die Grundlagen der Automatentheorie aus der Vorlesung "Theoretische Informatik" bekannt sein. Des Weiteren sollte die Motivation, Scala zu lernen, vorhanden sein.
Literature - Literatur
[1] Lorenzo Clemente und Richard Mayr: Advanced Automata Minimization