Tree-walking automaton

A tree-walking automaton (TWA) is a type of finite automaton that deals with tree structures rather than strings. The concept was originally proposed by Aho and Ullman.
The following article deals with tree-walking automata. For a different notion of tree automaton, closely related to regular tree languages, see branching automaton.
Definition.
All trees are assumed to be binary, with labels from a fixed alphabet Σ.
Informally, a tree-walking automaton (TWA) "A" is a finite state device that walks over an input tree in a sequential manner. At each moment "A" visits a node "v" in state "q". Depending on the state "q", the label of the node "v", and whether the node is the root, a left child, a right child or a leaf, "A" changes its state from "q" to "q"' and moves to the parent of "v" or its left or right child. A TWA accepts a tree if it enters an accepting state, and rejects if its enters a rejecting state or makes an infinite loop. As with string automata, a TWA may be deterministic or nondeterministic.
More formally, a (nondeterministic) tree-walking automaton over an alphabet Σ is a tuple
where "Q" is a finite set of states, its subsets "I", "F", and "R" are the sets of initial, accepting and rejecting states, respectively, and is the transition relation.
Example.
A simple example of a tree-walking automaton is a TWA that performs depth-first search (DFS) on the input tree. The automaton formula_1 has three states, formula_2. formula_1 begins in the root in state formula_4 and descends to the left subtree. Then it processes the tree recursively. Whenever formula_1 enters a node formula_6 in state formula_7, it means that the left subtree of formula_6 has just been processed, so it proceeds to the right subtree of formula_6. If formula_1 enters a node formula_6 in state formula_12, it means that the whole subtree with root formula_6 has been processed and formula_1 walks to the parent of formula_6 and changes its state to formula_7 or formula_12, depending on whether formula_6 is a left or right child.
Properties.
Unlike branching automata, tree-walking automata are difficult to analyze: even simple properties are nontrivial to prove. The following list summarizes some known facts related to TWA: