Umwandlung: 2-Wege Alternierende Büchi-Automaten in Nicht-deterministische Büchi-Automaten

Abstract - Zusammenfassung

Verschiedene Automatentypen werden als Zwischenschritte für die Umwandlung von Logiken in Monitore für Runtime-Verification genutzt. In diesem Fall wird die Umwandlung von pRLTL-Formeln in deterministische Moore-Maschinen betrachtet. Dabei werden viele Formeln sehr ineffizient über Paritätsautomaten umgewandelt, weshalb eine Umwandlung von 2-Wege Alternierende Büchi-Automaten (2ABA) in Nicht-deterministische Büchi-Automaten (NBA) benötigt wird.

Problem Statement - Beschreibung

Mit der Logik- und Automatenbibliothek RltlConv können Formeln verschiedener Logiken in Automaten und Automaten in andere Automaten umgewandelt werden. Insbesondere ist es aber möglich, für verschiedene Semantiken der Logiken Monitore (Moore- oder Mealy-Maschinen) zu generieren, die für die Verifikation von Programmen mittels Runtime-Verification genutzt werden können. Um die Formeln der, von Leucker und Sánchez entwickelten, Regular Linear Temporal Logic with past (pRLTL) für Runtime-Verification nutzen zu können, wird eine Umwandlung einer pRLTL-Formel in eine deterministische Moore-Maschine (DMM) benötigt. Auf dem Weg zur DMM werden die Formeln nacheinander in verschiedenste Automatentypen transformiert. Dabei gibt es den sehr ineffizienten Zwischenschritt von pRLTL-Formeln zu 2-Wege Alternierenden 3-Paritätsautomaten, der nur für wenige pRLTL-Formeln wirklich benötigt wird. Stattdessen würde eine Transformation in 2-Wege Alternierende Büchi-Automaten (2ABA) genügen. Es fehlt allerdings eine Implementierung der Umwandlung von 2ABAs in 1-Wege Nicht-deterministische Büchi-Automaten (NBA) aus [1], weshalb diese in dieser Arbeit vorgenommen werden soll.

Goals - Ziele

• Das Zusammenfassen der Umwandlung von einem 2ABA in einen NBA aus [1].
• Das Implementieren der Umwandlung in Scala.

Workplan - Vorgehen

1. Mit den benötigten Automatentypen (NBA,ABA,2ABA) und deren Eigenschaften vertraut machen.
2. Mit [1], sowie weiteren Publikationen, die aus [1] referenziert und für die Umwandlung benötigt werden, vertraut machen.
3. Zusammenfassen der, in den verschiedenen Publikationen beschriebenen, Umwandlungen in eine kompakte Form.
4. Überlegen einer Grundstruktur des Programms für eine möglichst effiziente Implementierung.
5. Implementieren der Umwandlung in Scala.

Requirements - Anforderungen

Es sollten die Grundlagen der Automatentheorie aus der Vorlesung "Theoretische Informatik" bekannt sein. Desweiteren sollte die Motivation, Scala zu erlernen, vorhanden sein.

Literature - Literatur

[1] Christian Dax und Felix Klaedtke: Alternation Elimination by Complementation