Existential second-order logic over strings

Existential second-order logic (ESO)and monadic second-order logic (MSO) ha ve attracted much interest in logic and computer science. ESO isa much more expressive logic over successor structures than MSG. However, little was k nown about the relationship between MSO and syntactic fragments of ESO. We shed light on this issue by completely characterizing this relationship for the prefix classes of ESO over strings, (i.e., finite successor structures ). Moreover, we determine the complexity of model checking over strings, fo r all ESO-prefix classes. Let ESO(2) denote the prefix class containing all sentences of the shape There Exists RQ phi, where R is a list of predicate variables, Q is a first-order quantifier prefix from the prefix set L, and phi is quantifier-free. We show that ESO(There Exists*For All There Exists *) and ESO(There Exists*For All For All) are the maximal standard ESO-prefi x classes contained in MSG, thus expressing only regular languages. We furt her prove the following dichotomy theorem: An ESO prefix-class either expre sses only regular languages (and is thus in MSO), ur it expresses some NP-c omplete languages. We also give a precise characterization of those ESO-pre fix classes that are equivalent to MSO over strings, and of the ESO-prefix classes which are closed under complementation on strings.