Infinite-tree automaton

In computer science and mathematical logic, an infinite-tree automaton is a state machine that deals with infinite tree structures. It can be seen as an extension of top-down finite-tree automata to infinite trees or as an extension of infinite-word automata to infinite trees.
A finite automaton which runs on an infinite tree was first used by Michael Rabin for proving decidability of monadic second-order logic. It has been further observed that tree automata and logical theories are closely connected and it allows decision problems in logic to be reduced into decision problems for automata.
Definition.
Infinite-tree automata work on formula_1-labeled trees. There are many slightly different definitions; here is one. A (nondeterministic) infinite-tree automaton is a tuple formula_2 with the following components.
An infinite-tree automaton is "deterministic" if for every formula_10, formula_11, and formula_17, the transition relation formula_18 has exactly one formula_13-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 formula_20 over a formula_1-labeled tree formula_22 is a formula_23-labeled tree formula_24 as follows. Suppose that the automaton reached a node formula_25 of an input tree and is currently in state formula_26. Let the node formula_25 be labeled with formula_28 and formula_29 be its branching degree. Then, the automaton proceeds by selecting a tuple formula_30 from the set formula_31 and cloning itself into formula_32 copies. For each formula_33, one copy of the automaton proceeds into node formula_34 and changes its state to formula_35. This produces a run which is a formula_7-labeled tree. Formally, a run formula_24 on the input tree satisfies the following two conditions.
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 formula_24, 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 formula_46, then the run is "accepting". Interesting accepting conditions are Büchi, Rabin, Streett, Muller, and parity. If for an input formula_1-labeled tree formula_48, there exists an accepting run, then the input tree is "accepted" by the automaton. The set of all accepted formula_1-labeled trees is called tree language formula_50 which is "recognized" by the tree automaton formula_20.
Expressive power of acceptance conditions.
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. (For example, there is no Büchi tree automaton that recognizes the set of formula_52-labeled trees whose every path has only finitely many formula_53s, see e.g. )
Furthermore, deterministic tree automata (Muller, Rabin, Streett, parity, Büchi, looping) 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 formula_53. 
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.