Paper: The Hierarchy inside Closed Monadic S1 Collapses on the Infinite Binary Tree (at LICS 2001)

Authors: Giacomo Lenzi André Arnold Jerzy Marcinkowski

Abstract

Closed monadic S1, as proposed in [AFS98], is the existential monadic second order logic where alternation between existential monadic second order quantifiers and first order quantifiers is allowed. Despite some effort very little is known about the expressive power of this logic on finite structures. We construct a tree automaton which exactly characterizes closed monadic S1 on the Rabin tree and give a full analysis of the expressive power of closed monadic S1 in this context. In particular, we prove that the hierarchy in-side closed monadic S1, defined by the number of alternations between blocks of first order quantifiers and blocks of existential monadic second order quantifiers collapses, on the infinite tree, to the level 2.

BibTeX

  @InProceedings{LenziArnoldMarcinko-TheHierarchyinsideC,
    author = 	 {Giacomo Lenzi and André Arnold and Jerzy Marcinkowski},
    title = 	 {The Hierarchy inside Closed Monadic S1 Collapses on the Infinite Binary Tree},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {157--166},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }