Characterization of \(\omega\)-regular languages by first-order formulas (Q800737)

An \(\omega\)-language over some finite alphabet A is a set of countable sequences over A. A finite automaton M can be used to define such languages; e.g. that M visits a certain state infinitely often while reading the sequence. With each finite automaton a first order language is associated. The atomic formulas are \(P_ s(t)\), \(t<t',\quad t=t',\) here t runs over a discrete time structure and \(P_ s(t)\) means that M is in state s at time t. The purpose of this paper is to compare two different kinds of definability for \(\omega\)-languages: Acceptance by various kinds of automata and definability by formulae with a bounded number of quantifier changes. Among the results proved are characterizations of co-regular languages in general and those satisfying certain conditions, e.g. being a countable union of closed sets.