Dot-Depth and Monadic Quantifier Alternation over Pictures

Oliver Matz

           In formulas of monadic second-order logic (MSO), quantifiers
           range over set of elements or over elements of the universe
           of some finite structure.

           Fagin has shown in 1974 that not every MSO-formula is
           equivalent to an existential one, i.e., a formula with a set
           quantifier prefix of existential set quantifiers only, followed
           by a first-order kernel formula (i.e. without set quantifiers).

           Fagin asked in 1995 whether in MSO-formulas the quantifier
           alternation depth of ``exist''-quantifiers on one hand and
           ``for-all''-quantifiers on the other hand can be bounded; in
           other words, whether there is a k>1 such that every MSO-formula
           is equivalent to one with a set quantifier prefix of k blocks
           of set quantifiers, existential and universal in alternation,
           followed by a first-order kernel formula.

           The thesis shows that this is not the case, even for a
           particular class of finite structure, the so-called ``grids''.
           Moreover, we investigate to what extent the alternation of
           first-order quantifiers is responsible for the increase of
           expressive power.

           The investigation of these questions yields as a
           by-product results about ``picture languages'', which are
           the two-dimensional analogue to classical (one-dimensional)
           languages.  In particular it is shown that there is a starfree,
           non-recognizable picture language, although both the notion
           of ``starfreeness'' and that of ``recognizability'' are
           straightforward generalizations of the corresponding notions
           is the setting of classical languages.