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 viewed as an extension from a finite tree automaton, which accepts only finite tree structures. It can also be viewed as an extension of some infinite word automatons such as the Büchi automaton and the Muller automaton.

A finite automaton which runs on an infinite tree was first used by Rabin for proving decidability of monadic second order logic. It has been further observed that tree automaton and logical theories are closely connected and it allows decision problems in logic to be reduced into decision problems for automata.

Definition

Infinite tree automaton runs of over a [math]\displaystyle{ \Sigma }[/math]-labeled tree. There are many slightly different formulations of tree automaton. Here one of the formulation is described. An infinite tree automaton is a tuple [math]\displaystyle{ A = (\Sigma, D, Q, \delta, q_0, F ) }[/math] where,

• [math]\displaystyle{ \Sigma }[/math] is an alphabet.
• [math]\displaystyle{ D\subset \mathbb{N} }[/math] is a finite set. Each element of [math]\displaystyle{ D }[/math] is an allowed degree in input tree.
• [math]\displaystyle{ Q }[/math] is a finite set of states.
• [math]\displaystyle{ \delta: Q \times \Sigma \times D \rightarrow 2^{Q^*} }[/math] is a transition relation that maps an automaton state [math]\displaystyle{ q \in Q }[/math], an input letter [math]\displaystyle{ \sigma \in \Sigma }[/math], and a degree [math]\displaystyle{ d \in D }[/math] to a set of d-tuple of states.
• [math]\displaystyle{ q_0 \in Q }[/math] is an initial state of automaton.
• [math]\displaystyle{ F \subseteq \Sigma^{\omega} }[/math] is an accepting condition.

Run

A run of tree automaton [math]\displaystyle{ A }[/math] over a [math]\displaystyle{ \Sigma }[/math]-labeled tree [math]\displaystyle{ (T,V ) }[/math] is a [math]\displaystyle{ Q }[/math]-labeled tree [math]\displaystyle{ (T_r, r ) }[/math]. Lets suppose that the tree automaton is at state [math]\displaystyle{ q }[/math] and it has reached to a node t labeled with [math]\displaystyle{ \sigma \in \Sigma }[/math] of input tree. [math]\displaystyle{ d(t) }[/math] is degree of node t. Then, the automaton proceeds by selecting a tuple [math]\displaystyle{ (q_1,...,q_{d(t)}) }[/math] from set [math]\displaystyle{ \delta( q, \sigma, d(t)) }[/math] and splitting into [math]\displaystyle{ d(t) }[/math] copies of itself. For each [math]\displaystyle{ 0 \lt i \leq d(t) }[/math], one copy enters into [math]\displaystyle{ q_i }[/math] state and proceeds to the node [math]\displaystyle{ t.i }[/math]. This process produces a run over a tree.

Formally, a run [math]\displaystyle{ (T_r, r ) }[/math] on the input tree satisfy following two conditions:

1. [math]\displaystyle{ r(\epsilon) = q_0 }[/math]
2. For every [math]\displaystyle{ t \in T_r }[/math] with [math]\displaystyle{ r(t) = q }[/math], there exists a [math]\displaystyle{ (q_1,...,q_{d(t)}) \in \delta(q,V(t),d(t)) }[/math] such that for every [math]\displaystyle{ 0 \lt i \leq d(t) }[/math], we have [math]\displaystyle{ t.i \in T_r }[/math] and [math]\displaystyle{ r(t.i) = q_i }[/math]

Acceptance condition

In a run [math]\displaystyle{ (T_r, r ) }[/math], 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 [math]\displaystyle{ F }[/math], then the run is accepting. The interesting accepting conditions are Büchi, Rabin, Streett and Muller. If for an input [math]\displaystyle{ \Sigma }[/math]-labeled tree [math]\displaystyle{ (T,V ) }[/math] there exist an accepting run then the input tree is accepted by the automaton. The set of all the accepted [math]\displaystyle{ \Sigma }[/math]-labeled trees is called tree language [math]\displaystyle{ \mathcal{L}(A) }[/math] which is recognized by tree automaton [math]\displaystyle{ A }[/math].

Remarks

The set D may seem unusual to some people. Some times D is omitted from the definition when it is a singleton set that means input tree has fixed branching at each node. For example, if D = {2} then the input tree has to be a full binary tree.

Infinite tree automaton is deterministic if for some [math]\displaystyle{ q \in Q }[/math], [math]\displaystyle{ \sigma \in \Sigma }[/math], and [math]\displaystyle{ d \in D }[/math] transition relation [math]\displaystyle{ \delta( q, \sigma, d) }[/math] has exactly one element. Otherwise the automaton is non-deterministic.

Accepting tree languages

Muller, parity, Rabin, and Streett accepting conditions in an infinite tree automaton recognize the same tree languages.

But, Büchi accepting condition is strictly weaker than other accepting conditions, i.e., there exists a tree language which can be recognized by Muller accepting condition in infinite tree automata but can't be recognized by any Büchi accepting condition in some infinite tree automaton.

Tree languages which are recognized by Muller accepting conditions are closed under union, intersection, projection and complementation.