Expressive power of existential first-order sentences of Büchiʹs sequential calculus Original Research Article

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