Infinite-tree automata work on -labeled trees. There are many slightly different definitions; here is one. A infinite-tree automaton is a tuple with the following components.
is an alphabet. This alphabet is used to label nodes of an input tree.
is a finite set of allowed branching degrees in an input tree. For example, if, an input tree has to be a binary tree, or if, then each node has either 1, 2, or 3 children.
is a finite set of states; is initial.
is a transition relation that maps an automaton state, an input letter, and a degree to a set of -tuples of states.
is an accepting condition.
An infinite-tree automaton is deterministic if for every,, and, the transition relation has exactly one -tuple.
Run
Intuitively, a run of a tree automaton on an input tree assigns automaton states to the tree nodes in a way that satisfies the automaton transition relation. A bit more formally, a run of a tree automaton over a -labeled tree is a -labeled tree as follows. Suppose that the automaton reached a node of an input tree and is currently in state. Let the node be labeled with and be its branching degree. Then, the automaton proceeds by selecting a tuple from the set and cloning itself into copies. For each, one copy of the automaton proceeds into node and changes its state to. This produces a run which is a -labeled tree. Formally, a run on the input tree satisfies the following two conditions.
.
For every with, there exists a such that for every, we have and.
If the automaton is nondeterministic, there may be several different runs on the same input tree; for deterministic automata, the run is unique.
Acceptance condition
In a run, an infinite path is labeled by a sequence of states. This sequence of states form an infinite word over states. If all these infinite words belong to accepting condition, then the run is accepting. Interesting accepting conditions are Büchi, Rabin, Streett, Muller, and parity. If for an input -labeled tree , there exists an accepting run, then the input tree is accepted by the automaton. The set of all accepted -labeled trees is called tree language which is recognizedby the tree automaton.
Nondeterministic Muller, Rabin, Streett, and parity tree automata recognize the same set of tree languages, and thus have the same expressive power. But nondeterministic Büchi tree automata are strictly weaker, i.e., there exists a tree language that can be recognized by a Rabin tree automaton but cannot be recognized by any Büchi tree automaton. Furthermore, deterministic tree automata are strictly less expressive than their nondeterministic variants. For example, there is no deterministic tree automaton that recognizes the language of binary trees whose root has its left or right child marked with. This is in sharp contrast to automata on infinite words, where nondeterministic Büchi ω-automata have the same expressive power as the others. The languages of nondeterministic Muller/Rabin/Streett/parity tree automata are closed under union, intersection, projection, and complementation.
