Characterization of ω-regular languages by first-order formulas

First-order formulas are used to specify various ways of acceptance of ω-languages by (deterministic) finite automata, and we study the relationship between the ‘arithmetic’ hierarchy of the formulas in prenex normal form and the topological hierarchy of the accepted ω-languages. Among other things it is proved that the ω-languages accepted by finite automata under the accepting conditions specified by Σ₁-type formulas are precisely open ω-regular languages, those accepted under the conditions specified by Σ₂-type formulas coincide with the ω-regular languages which are denumerable unions of closed sets, and that as long as the accepting conditions are specified by first-order formulas the accepted ω-languages remain to be ω-regular.