LTL is a star-free language but it can describe $a^*b^\omega$. Contradiction?

Question

Does the statement "LTL is a star-free language"(from wiki) mean that the expressiveness power of LTL is equivalent to that of star-free languages? Then why can you describe in LTL the following language with the star: $a^*b^\omega$? $$\mathbf{G}(a \implies a\mathbf{U}b) \land G(b \implies \mathbf{X}b)$$ So, what does the sentence "LTL is star-free language" mean? Can you give an example of regular language with star which cannot be expressed in LTL? (not an example of LTL < NBA, but an example of LTL < regular language with star)

Answer 1

Short answer: $a^*b^{\omega}$ describes a star-free language.

Longer answer:

In order to show that let's consider two definitions of a regular star-free language :

• Language has a maximum star height of 0.
• Language is in the class of star-free languages, which is defined as follows: it's the smallest subset of $\Sigma^{\omega}$ which contains $\Sigma^{\omega}$, all singletons $\{x\}$, $x \in \Sigma$, and which is closed under finite union, concatenation and complementation.

It's possible to see that those two definitions are equivalent. We can also note that all finite languages are star-free.

An $\omega$-regular language is called $\omega$-star-free if it's a finite union of languages of type $XY^{\omega}$, where $X$ and $Y^+$ are star-free.

Now, $L = a^*$ can be described as $\Sigma^* \setminus (\Sigma^* (\Sigma \setminus a) \Sigma^*)$, so $L$ is a star-free language. Since $L' = a^* b^{\omega}$ can be written as concatenation in the form of $XY^{\omega}$ where $X = L$ and $Y = \{b\}$ (it's easy to show that $Y^+$ is star-free) we can conclude that $L'$ is star-free.

For more information (and equivalent definitions) I can refer you to the following papers: First-order definable languages, On the Expressive Power of Temporal Logic, On the expressive power of temporal logic for infinite words

Answer 2

Indeed, the language $a^*b^\omega$ is star-free, and it can be equivalently captured by $L_1L_2$, where $$L_1=\Sigma^*b\backslash(\Sigma^*(\Sigma\backslash a)\Sigma^*b)$$ and $$L_2=\Sigma^\omega\backslash(\Sigma^*(\Sigma\backslash b)\Sigma^\omega).$$ In the above, $L_1$ and $L_2$ are respectively equal to $a^*b$ and $b^\omega$.

Note that for star-free expressions, Kleen-closure ($*$ and $\omega$) can only be applied to $\Sigma$ (the whole alphabet set).

B.T.W., you may simplify your LTL expression, and you can just use $a{\bf U}({\bf G}b)$.