Paper: A Contraction Method to Decide MSO Theories of Deterministic Trees (at LICS 2007)

Authors: Angelo Montanari Gabriele Puppis

Abstract

In this paper we generalize the contraction method, originally proposed by Elgot and Rabin and later extended by Carton and Thomas, from labeled linear orderings to colored deterministic trees. The method we propose rests on a suitable notion of indistinguishability of trees with respect to tree automata that allows us to reduce a number of instances of the acceptance problem for tree automata to decidable instances involving regular trees. We prove that such a method works effectively for a large class of trees, which is closed under noticeable operations and includes all the deterministic trees of the Caucal hierarchy obtained via unfoldings and inverse finite mappings as well as several trees outside such a hierarchy.

BibTeX

  @InProceedings{MontanariPuppis-AContractionMethodt,
    author = 	 {Angelo Montanari and Gabriele Puppis},
    title = 	 {A Contraction Method to Decide MSO Theories of Deterministic Trees},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {141--150},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }