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.

However, there are ways to tackle this problem. You can start here for a reference.

  • $\begingroup$ Is there an algorithm that convert an $\omega$-regular expression to its equivalent Buchi automaton? $\endgroup$ – Perissiane Jan 18 '17 at 16:20
  • $\begingroup$ Sure. It's almost identical to the corresponding algorithm for regular expressions and DFAs. Just construct recursively. $\endgroup$ – Shaull Jan 18 '17 at 16:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.