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 trees. It can also be viewed as an extension of infinite-word automata such as Büchi automata and Muller automata.

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 automata work on $\Sigma$-labeled trees. There are many slightly different definitions; here is one. A (nondeterministic) infinite-tree automaton is a tuple $A=(\Sigma ,D,Q,\delta ,q_{0},F)$ with the following components.

• $\Sigma$ is an alphabet. This alphabet is used to label nodes of an input tree.
• $D\subset \mathbb {N}$ is a finite set of allowed branching degrees in an input tree.
• $Q$ is a finite set of states.
• $\delta :Q\times \Sigma \times D\rightarrow 2^{Q^{*}}$ is a transition relation that maps an automaton state $q\in Q$, an input letter $\sigma \in \Sigma$, and a degree $d\in D$ to a set of $d$-tuples of states.
• $q_{0}\in Q$ is an initial state of automaton.
• $F\subseteq \Sigma ^{\omega }$ is an accepting condition.

Run

A run of a tree automaton $A$ over a $\Sigma$-labeled tree $(T,V)$ is a $Q$-labeled tree $(T_{r},r)$. Suppose that the tree automaton reached a node $t$ of an input tree and it is currently in state $q$. Let the node be labeled with $\sigma \in \Sigma$ and $d(t)$ be its branching degree. Then, the automaton proceeds by selecting a tuple $(q_{1},...,q_{d(t)})$ from the set $\delta (q,\sigma ,d(t))$ and splitting itself into $d(t)$ copies. For each $0<i\leq d(t)$, one copy of the automaton proceeds into node $t.i$ and changes its state to $q_{i}$. This produces a run which is a $Q$-labeled tree. Intuitively, the run replaces each node label from $\Sigma$ by a label from $Q$ in a way that satisfies the transition relation of the automaton.

Formally, a run $(T_{r},r)$ on the input tree satisfies the following two conditions.

• $r(\epsilon )=q_{0}$.
• For every $t\in T_{r}$ with $r(t)=q$, there exists a $(q_{1},...,q_{d(t)})\in \delta (q,V(t),d(t))$ such that for every $0<i\leq d(t)$, we have $t.i\in T_{r}$ and $r(t.i)=q_{i}$.

There may be several different runs on the same input tree.

Acceptance condition

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

Remarks

The set $D$ may seem unusual. Sometimes $D$ is omitted from the definition when it is a singleton set, which means the input trees have a fixed branching degree at each node. For example, if $D=\{2\}$, then the input tree has to be a full binary tree.

An infinite tree automaton is deterministic if for every $q\in Q$, $\sigma \in \Sigma$, and $d\in D$, the transition relation $\delta (q,\sigma ,d)$ has exactly one element. Otherwise the automaton is non-deterministic.

Expressive power

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.