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

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 Σn-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 BΣ1, the boolean combinations of existential formulas. We also give an O(n7)-time algorithm to decide whether the language accepted by a deterministic n-state automaton is expressible by a first-order sentence (respectively, a BΣ1-sentence).