LTL translation to omega-regular languages

Question

I tried to define a translation from LTL to ω-regular languages. I built it inductively on the structure of LTL formulae. No problem except with the 'until' operator where I came up with the expression:

$$ L_\omega(f \mathbf{U} g) = \bigcup_{k\ge 0} \biggl( \bigl(\bigcap_{0\le j\le k-1} \Sigma^j L_\omega(f)\bigr) \cap \Sigma^k L_\omega(g) \biggr) $$

where $L_\omega(f)$, $L_\omega(g)$ are $\omega$-regular, $\Sigma^j$ is a symbol from $\Sigma$ repeated $j$ times (where $\Sigma$ is the set of language symbols). The problem with this expression is that it is a countable union of $\omega$-regular languages. Are $\omega$-regular languages closed under countable union? (reference to a proof). Otherwise, can somebody suggest another expression (I tried also a recursive expression based on the identity $f \cup g = g \vee (f \wedge O(f \cup g))$ but then the same question with respect to recursive expressions?

Answer 1

Given a word $u \in \Sigma^\omega$, write $u_n$ for its $n$th symbol and $\bar u_n$ for its prefix of length $n$. Let $u \in \Sigma^\omega$ be an arbitrary word. $$ \bigcap_{n\in\mathbb{N}} \{\bar u_n\}\Sigma^\omega = \{v \mid \forall i \le n, v_i = u_i\} = \{u\} $$ Thus an arbitrary word can be expressed as a countable intersection of $\omega$-regular languages. (This is similar to expressing a real number as the limit of its expansion in base $|\Sigma|$.) There are uncountably many words in $\Sigma^\omega$, but only countably many $\omega$-regular languages since there are only countably many Büchi automata to recognize them. Therefore countable intersections of $\omega$-regular are not always (indeed almost never) $\omega$-regular. Since $\omega$-regular languages are closed under complementation, the same goes for countable unions.

In any case, you won't be able to find such a translation, because LTL is not quite as expressive as Büchi automata: there are $\omega$-regular properties that cannot be defined in LTL. Extensions of LTL have been proposed that can express all $\omega$-regular properties. See Temporal Logic can be more expressive, Pierre Wolper, Information and Computation, 1983. (via Vijay D in Equivalence of Büchi automata and linear μ\mu-calculus on Computer Science Stack Exchange)