Decidability of MSO Theories of Tree Structures

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.

• Type: Conference
• Year: 2004
• Where: FSTTCS
• Authors: Angelo Montanari, Gabriele Puppis
• Keywords: Deterministic Tree Structures, FSTTCS 2004, Monadic Second-order Theories, Regular Trees