Regular Linear Temporal Logic (RLTL) is a temporal logic that extends the expressive power of Linear Temporal Logic (LTL) to all w-regular languages. This extension is achieved using only a first-order signature, without the need of fix-point operators or automata-like operators. Moreover, all operators of LTL and w-regular-expressions are translated linearly, as contexts with the same number of “holes”. RLTL is based on the fundamental idea of an operator that generalizes controlled repetition. In this talk I will present two new results on RLTL, namely: (1) a variation of RLTL which allows negation normal forms, and (2) a translation of RLTL into alternating parity automata on words using only 3 colors, which is in fact a generalization of hesitant automata.

The talk is structured in two parts (of roughly 30 minutes each). In the first part, I will present some connections between automata theory on infinite words, temporal logics and games. I will use these results in the second part of the talk, in which I will sketch our results.