We present regular linear temporal logic (\RLTL), a logic that generalizes linear temporal logic with the ability to use regular expressions arbitrarily as sub-expressions. Every LTL operator can be defined as a context in regular linear temporal logic. This implies that there is a (linear) translation from LTL to \RLTL. Unlike LTL, regular linear temporal logic can define all $\omega$-regular languages, while still keeping the satisfiability problem in PSPACE. Unlike the extended temporal logics $\text{ETL}_*$, \RLTL is defined with an algebraic signature. In contrast to the linear time \MuCalculus, \RLTL does not depend on fix-points in its syntax.
In Proceedings of The 4th International Colloquium on Theoretical Aspects of Computing (ICTAC'07), vol. 4711 of Lecture Notes in Computer Science (LNCS), pp 291--305. Springer, 2007.