Equations Over ω-Automata
An infinite word over an alphabet A, or ω-word, is an infinite sequence of symbols of A. Aω is the set of ω-words on A. An ω-language on A is a subset of Aω. Moreover, A ∞ = A⋆ ∪Aω. An ω-word may be written as \(\alpha = \alpha (0)\alpha (1)\ldots \), where α(i) ∈ A for every i ≥ 0; if n ≤ m, \(\alpha (n,m) = \alpha (n)\ldots \alpha (m - 1)\alpha (m)\) and \(\alpha (n,\infty ) = \alpha (n)\alpha (n + 1)\ldots \). The notations ∃ωn stands for ’there are infinitely many n’ and ∃< ωn stands for ’there are finitely many n’.