Transformation of Regular Linear Temporal Logic into Parity Automata
for Degree:
Contact Person:
Status:
Completed
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.