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?