Logical specifications of infinite computations

Abstract

Starting from an identification of infinite computations with wwords, we present a framework in which different classification schemes for specifications axe 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 w-automata. In particular, it is shown in which sense these hieraxchies 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 w-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 w-words are taken as model of computation).