Logical specifications of infinite computations

Starting from an identification of infinite computations with ω-words, we present a framework in which different classification schemes for specifications are naturally compared. Thereby we connect logical formalisms with hierarchies of descriptive set theory (e.g., the Borel hierarchy), of recursion theory, and with the hierarchy of acceptance conditions of ω-automata. In particular, it is shown in which sense these hierarchies can be viewed as classifications of logical formulas by the complexity measure of quantifier alternation. In this context, the automaton theoretic approach to logical specifications over ω-words turns out to be a technique to reduce quantifier complexity of formulas. Finally, we indicate some perspectives of this approach, discuss variants of the logical framework (first-order logic, temporal logic), and outline the effects which arise when branching computations are considered (i.e., when infinite trees instead of ω-words are taken as model of computation).