Is there any systematic (algorithmic) method to convert an $\omega$-regular expression like
$ (a^∗)(b)(b^∗)(a^∗)(c^\omega) $
to an LTL property?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
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$ Commented Jan 18, 2017 at 16:20
-
$\begingroup$ Sure. It's almost identical to the corresponding algorithm for regular expressions and DFAs. Just construct recursively. $\endgroup$– ShaullCommented Jan 18, 2017 at 16:42