Is there any systematic (algorithmic) method to convert an $\omega$-regular expression like
$ (a^∗)(b)(b^∗)(a^∗)(c^\omega) $
to an LTL property?
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community
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.
However, there are ways to tackle this problem. You can start here for a reference.