Vierwertige RLTL Semantik auf endlichen Worten

Abstract - Zusammenfassung

Analog zu der vierwertigen LTL-Semantik auf endlichen Worten soll eine entsprechende Semantik für RLTL entwickelt werden. Des Weiteren soll ein Automatenmodell für die neu entwickelte Semantik angegeben und die Umwandlung in das Automatenmodell implementiert werden.

Problem Statement - Beschreibung

Die Regular Linear Temporal Logic (RLTL) wurde von Leucker und Sánchez in [1] entwickelt. RLTL ist eine Erweiterung von der Linear Temporal Logic (LTL) um reguläre Ausdrücke und bietet dadurch eine höhere Ausdrucksstärke als LTL. Die Semantiken beider Logiken sind auf unendlichen Worten definiert. Wenn die korrekte Funktionalität eines Systems während der Laufzeit mittels Runtime-Verification überprüft werden soll, ist allerdings zu jedem Zeitpunkt immer nur ein endlicher Präfix des gesamten Laufes des Systems vorhanden. Das heißt, dass nur auf diesem endlichen Präfix überprüft werden kann, ob sich das System bisher korrekt verhält. Aus diesem Grund wurde LTL in [2,3] zu einer Variante auf endlichen Worten, genannt FLTL, verändert. FLTL hat aber nur zwei Ergebniswerte. Diese reichen nicht aus, damit für eine Eigenschaft festgestellt werden kann, ob sie in diesem endlichen Präfix endgültig verletzt oder erfüllt wurde oder ob dies noch unklar ist. Dafür werden vier mögliche Ergebniswerte benötigt, weshalb FLTL noch zu der vierwertigen Variante FLTL4 ([2,3]) erweitert wurde. Dabei gibt es neben den zwei endgültigen Wahrheitswerten noch zwei weitere, die angeben, welches der Ausgabewert wäre, wenn der Lauf des Systems zu dem aktuellen Zeitpunkt enden würde.

Eine solche vierwertige Semantik auf endlichen Worten fehlt für RLTL noch und soll in dieser Arbeit entwickelt werden. Außerdem können FLTL4-Formeln direkt in alternierende Mealy-Maschinen (AMM) umgewandelt werden, welche dann den Monitor darstellen. Eine entsprechende Umwandlung in AMMs soll auch für die neue Semantik von RLTL konstruiert werden. Als letztes soll dann die Umwandlung der neuen Semantik in die AMM in die Logik- und Automatenbibliothek RltlConv implementiert werden. RltlConv beherrscht bereits die Monitorgenerierung für verschiedene Semantiken von LTL und RLTL, unter anderem auch die von FLTL4. Aus diesem Grund muss nur der Algorithmus für die Umwandlung implementiert werden, da RLTL sowie AMMs bereits als Datenstrukturen vorhanden sind.

Goals - Ziele

• Entwicklung einer vierwertigen RLTL Semantik auf endlichen Worten
• Entwicklung eines Automatenmodells dieser Semantik
• Implementieren der Umwandlung der neuen Semantik in das Automatenmodell in Scala

Workplan - Vorgehen

1. Mit FLTL4 und RLTL vertraut machen
2. Entwickeln einer Semantik für eine vier-wertige Erweiterung von RLTL
3. Mit dem Automatenmodell von FLTL4 vertraut machen
4. Ein Automatenmodell für die vier-wertige Erweiterung von RLTL konstruieren
5. Mit der Struktur der Logik- und Automatenbibliothek RltlConv vertraut machen
6. Implementieren der Semantik und des Automatenmodells in Scala

Requirements - Anforderungen

Vorkenntnisse über die Linear Temporal Logic (LTL) sind von Vorteil aber keine Pflicht. Mealy-Maschinen sollten bekannt sein. Des Weiteren sollte die Motivation, Scala zu lernen, vorhanden sein.

Literature - Literatur

[1] Martin Leucker und César Sánchez: Regular Linear Temporal Logic

[2] Martin Leucker: Teaching Runtime Verification

[3] Martin Leucker: Runtime-Verification Vorlesungsskript