Tree Automaton - Definitions

Definitions

A ranked alphabet is a pair of ordinary alphabet and a function . Each letter has its arity so it can be used to build terms. Nullary elements (of zero arity) are also called constants. Terms built with unary symbols and constants can be considered as strings. Higher arity leads to trees.

A bottom-up finite tree automaton over is defined by:

Here is a set of unary letters (states), is a ranked alphabet, is a set of final states, and is a set of transition rules, that is, rewrite rules from nodes whose childs' roots are states, to nodes whose roots are states. Thus the state of a node is deduced from the states of its children.

There is no initial state as such, but the transition rules for constant symbols (leaves) can be considered as initial states. The tree is accepted if the state labeled at the root is an accepting state.

A top-down finite tree automaton over is defined by:

There are two differences with bottom-up tree automata : first, the set of its initial states, replaces ; second, its transition rules are the converse, that is, rewrite rules from nodes whose roots are states to nodes whose child's roots are states. The tree is accepted if every branch can be gone through this way.

The rewrite rules cause symbols from to 'travel' along branches of the tree.

One can easily guess that non-deterministic top-down tree automata are equivalent to non-deterministic bottom-up ones ; the transition rules are simply reversed, and the final states become the initial states.

Why then are deterministic top-down FTA less powerful than their bottom-up counterparts? Because a deterministic TA is by definition one where no two transition rules have the same left-hand side. For tree automata, transition rules are rewrite rules ; and for top-down ones, the left-hand side will be parent nodes. Consequently a deterministic top-down tree automaton will only be able to test for tree properties that are true in all branches, because the choice of the state to write into each child branch is determined at the parent node, without knowing the child branches contents.