Umwandlung: 2-Wege Alternierende 3-Paritätsautomaten 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, für die noch eine Umwandlung von 2-Wege Alternierenden 3-Paritätsautomaten (2A3PA) in Nicht-deterministische Büchi-Automaten (NBA) fehlt, welche in dieser Arbeit entwickelt und programmiert werden soll.

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. Zuerst muss eine pRLTL-Formel dafür in einen 2-Wege Alternierenden 3-Paritätsautomaten (2A3PA) umgewandelt werden. Es fehlt allerdings eine Umwandlung von 2A3PAs in Nicht-deterministische Büchi-Automaten (NBA), damit aus den NBAs die DMM generiert werden kann. Aus diesem Grund soll die Umwandlung von 2A3PAs in NBAs in dieser Arbeit entwickelt und implementiert werden. Eine Umwandlung von 1-Wege Alternierenden 3-Paritätsautomaten in NBAs wird, zum Beispiel, in [1] beschrieben. Diese ist allerdings sehr ineffizient. Umwandlungen von 2-Wege in 1-Wege Automaten werden unter anderem in [2] dargestellt.

Goals - Ziele

• Das Entwickeln einer möglichst effizienten Umwandlung von 2A3PAs in NBAs.
• Das Implementieren dieser Umwandlung in Scala.

Workplan - Vorgehen

1. Mit den benötigten Automatentypen (NBA,A3PA,2A3PA) und deren Eigenschaften vertraut machen.
2. Eine Literaturrecherche nach bisherigen Umwandlungen von ähnlichen Automatentypen in NBAs durchführen, wie z.B. die aus [1] und [2].
3. Eine neue Umwandlung (möglicherweise auf Basis der bei der Recherche gefundenen) entwickeln.
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] Cesar Sanchez, Julian Samborski-Forlese: Efficient Regular Linear Temporal Logic using Dualization and Stratification

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