Transformation of Regular Linear Temporal Logic into Parity Automata

for Degree: 
Contact Person: 

The author of this thesis is Malte Schmitz.

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.