Expressive power of existential first-order sentences of Büchi's sequential calculus

Abstract: The aim of this paper is to study the first-order theory of the successor, interpreted on finite words. More specifically, we are interested in the hierarchy based on quantifier alternations (or -hierarchy). It was known (J. Comput. Syst. Sci. 25 (1982) 360–375) that this hierarchy collapses at level 2, but the expressive power of the lower levels was not characterized effectively. We give a semigroup theoretic description of the expressive power of , the boolean combinations of existential formulas. We also give an -time algorithm to decide whether the language accepted by a deterministic n-state automaton is expressible by a first-order sentence (respectively, a -sentence). [Copyright &y& Elsevier]