In this paper we provide an automaton-based solution to the decision problem for a large set of monadic second-order theories of deterministic tree structures. We achieve it in two steps: first, we reduce the considered problem to the problem of determining, for any Rabin tree automaton, whether it accepts a given tree; then, we exploit a suitable notion of tree equivalence to reduce (a number of instances of) the latter problem to the decidable case of regular trees. We prove that such a reduction works for a large class of trees, that we call residually regular trees. We conclude the paper with a short discussion of related work. © Springer-Verlag Berlin Heidelberg 2004.
CITATION STYLE
Montanari, A., & Puppis, G. (2004). Decidability of MSO theories of tree structures. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3328, 434–446. https://doi.org/10.1007/978-3-540-30538-5_36
Mendeley helps you to discover research relevant for your work.