Twelfth Annual IEEE Symposium on

Logic in Computer Science (LICS 1997)

Paper: The Monadic Quantifier Alternation Hierarchy over Graphs is Infinite (at LICS 1997)

Authors: Oliver Matz Wolfgang Thomas

Abstract

We show that in monadic second-order logic over finite directed graphs, a strict hierarchy of expressiveness is obtained by increasing the (second-order) quantifier alternation depth of formulas. Thus, the ``monadic analogue'' of the polynomial hierarchy is found to be strict, which solves a problem of Fagin. The proof is based on automata theoretic concepts (rather than Ehrenfeucht-Fraiss'e games) and starts from a restricted class of graph-like structures, namely finite two-dimensional grids. We investigate monadic second-order definable sets of grids where the width of grids is a function of the height. In this context, the infiniteness of the quantifier alternation hierarchy is witnessed by n-fold exponential functions for increasing n. It is notable that these witness sets of the monadic hierarchy all belong to the complexity class NP, the first level of the polynomial hierarchy.

BibTeX

  @InProceedings{MatzThomas-TheMonadicQuantifie,
    author = 	 {Oliver Matz and Wolfgang Thomas},
    title = 	 {The Monadic Quantifier Alternation Hierarchy over Graphs is Infinite},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {236--244},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }