Transformation von regulärer Linearzeit-Temporallogik zu Paritätsautomaten

Bachelorarbeit am Institut für Softwaretechnik und Programmiersprachen (ISP) der Universität zu Lübeck. Ausgegeben und betreut von Prof. Dr. Martin Leucker.

Kurzfassung Reguläre Linearzeit-Temporallogik (RLTL) vereinigt die Vorteile von linearer Temporallogik (LTL) und ω-regulären Ausdrücken in einer neuen Logik. Um RLTL in der Praxis verwenden zu können, wird eine effiziente Umwandlung von RLTL zu Automaten benötigt. Im Rahmen dieser Arbeit wurde ein Scala-Programm implementiert, das RLTL-Formeln einliest und zu endlichen alternierenden Zwei-Wege-Paritätsautomaten umwandelt. In dieser Arbeit wird die verwendete Umwandlung und deren Implementierung detailliert beschrieben.

Abstract Regular linear temporal logic (RLTL) combines the advantages of linear temporal logic (LTL) and ω-regular expressions in a new logic. To use RLTL in practise an efficient translation from RLTL into automata is needed. In the context of this thesis such a translation was implemented as a scala program, which reads in RLTL formulas and translates them into finite alternating two-way parity au- tomata. In this thesis the used translation and its implementation will be described in detail.

Die Software LamaConv aus dieser Arbeit wird kontinuierlich weiter entwickelt und auf der Website des Projektes veröffentlicht. Sie wird unter anderem auch in LEGO® meets RV verwendet.

Meine Interesse für (reguläre) Linearzeit-Temporallogik und deren Automatenmodelle wurde zum ersten Mal in der Veranstaltung Präsentieren und Dokumentieren geweckt. Diese Veranstaltung an der Universität zu Lübeck soll den Studenten dabei helfen, ein geeignetes Thema für die Bachelorarbeit zu finden. Im Rahmen dieser Veranstaltung habe ich einen Kurzvortrag über die Regular Linear Temporal Logic (RLTL) gehalten.

Ziele des Vortrags

1. Schwäche von LTL gegenüber reg. Ausdrücken erkennen
2. RLTL kennen lernen
3. die Power-Operatoren verstehen
4. Umwandlung von ω-reg. Ausdrücken und LTL zu RLTL sehen

Zusammenfassung des Vortrags

1. RLTL vereint LTL und ω-reguläre Ausdrücke. Beide können in RLTL überführt werden.
2. RLTL kann alle ω-regulären Sprachen beschreiben.
3. Die Power-Operatoren aus RLTL verallgemeinert die N-, G-, F-, U-, R-Operatoren aus LTL und den ω-Operator aus ω-regulären Ausdrücken.