We investigate the question whether the wel-known correspondence between tree automata nad the weak second order logic of two successor functions (WS2S) can be extended to tree automata with tests. Our first insight is that there is no generalization of tree automata with tests that has a decidable emptiness problem and that is equivalent to the full class of formulae in some extension of WS2S, at least not when we are asking for an conservative extension of the classical correspondence between WS2S and tree automata to tree automata with tests. As a consequence we can extend the correspondence between tree automata and WS2S to automata with tests only when we admit a restriction of the class of formulae. We present a logic, called WS2Sy, and a restriction of the class of formula, called uniform, that is equivalent to tree automata with tests.
展开▼
