# $\omega$-regular expression to LTL

Is there any systematic (algorithmic) method to convert an $\omega$-regular expression like

$(a^∗)(b)(b^∗)(a^∗)(c^\omega)$

to an LTL property?

LTL is less expressive than $\omega$-regular expressions. For example, the expression $$((a+b)b)^\omega$$ i.e. "there is $b$ in all the even places" cannot be expressed in LTL.
In addition, observe that checking whether an $\omega$ regular expression is expressible in LTL is harder than checking universality, which is PSPACE hard.
• Is there an algorithm that convert an $\omega$-regular expression to its equivalent Buchi automaton? – Perissiane Jan 18 '17 at 16:20