loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
A Contraction Method to Decide MSO Theories of Deterministic Trees
Wroclaw, Poland
July 10-July 14
ISBN: 0-7695-2908-9
Angelo Montanari, Universita di Udine, Italy
Gabriele Puppis, Universita di Udine, Italy
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.
Citation:
Angelo Montanari, Gabriele Puppis, "A Contraction Method to Decide MSO Theories of Deterministic Trees," lics, pp.141-150, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.