Dreiwertige Timed-LTL-Semantik

Zusammenfassung

Es soll die dreiwertige Semantik für die Timed Linear Temporal Logic betrachtet sowie das passende Automatenmodell, welches die Eigenschaften der Semantik wiederspiegelt, untersucht werden. Außerdem soll die Umwandlung der Formeln der dreiwertigen Semantik in das Automatenmodell in die Logik- und Automatenbibliothek RltlConv implementiert werden.

Beschreibung

Für die Verifikation von Programmen während der Laufzeit (Runtime-Verification, RV) wird eine Spezifikationssprache benötigt, mit der die zu überwachenden Eigenschaften angegeben werden können. Danach wird aus den Formeln abhängig von der gewählten Semantik ein Automat generiert, der dann für die RV genutzt werden kann.

Die Logik- und Automatenbibliothek RltlConv, die am ISP entwickelt wurde, beherrscht den vorher genannten Ablauf bereits für verschiedene Logiken, zum Beispiel für die Linear Temporal Logic (LTL) sowie drei- und vierwertige Semantiken dieser. Es fehlt aber eine Logik, mit der auch Echtzeiteigenschaften ausgedrückt werden können. Da es mit der Timed Linear Temporal Logic (siehe [1], dort EventClockTL genannt) möglich ist, solche Eigenschaften zu spezifizieren, ist eine Erweiterung von RltlConv um diese Logik sinnvoll. Wie LTL besitzt auch TLTL erstmal nur eine zweiwertige Semantik über unendlichen Worten. In [2] wurde LTL um eine dreiwertige Semantik auf endlichen Worten (LTL3) erweitert. In der Semantik gibt es zwei endgültige Wahrheitswerte und diese werden so früh wie möglich erkannt, anders als bei einer vierwertigen Semantik. Dafür ist die Generierung der Automaten in der dreiwertigen Semantik deutlich komplizierter als in einer vierwertigen.

In der MA soll die dreiwertige TLTL-Semantik aus [2] genutzt, das dort angegebene Automatenmodell genauer untersucht und Möglichkeiten für eine Implementierung betrachtet werden. Außerdem soll die Umwandlung von Formeln für die Semantik in das passende Automatenmodell in RltlConv implementiert werden.

Ziele

•  Das Betrachten der dreiwertigen TLTL-Semantik und das Untersuchen des Automatenmodells.
•  Das Implementieren der Umwandlung in Scala.

Anforderungen

Es sollten die Grundlagen der Automatentheorie, wie zum Beispiel aus der Vorlesung "Theoretische Informatik", bekannt sein. Des Weiteren sollte die Motivation, Scala zu erlernen, vorhanden sein.

Literatur

[1] Thomas Henzinger, Jean-François Raskin und Pierre Yves Schobbens: Logics, Automata and Classical Theories for Deciding Real Time Languages
[2] Andreas Bauer, Martin Leucker und Christian Schallhart: Runtime Verification for LTL and TLTL