Infinite tree automaton

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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[1] 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.


Infinite tree automaton runs of over a -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 where,

  • is an alphabet.
  • is a finite set. Each element of is an allowed degree in input tree.
  • is a finite set of states.
  • is a transition relation that maps an automaton state , an input letter , and a degree to a set of d-tuple of states.
  • is an initial state of automaton.
  • is an accepting condition.


A run of tree automaton over a -labeled tree is a -labeled tree . Lets suppose that the tree automaton is at state and it has reached to a node t labeled with of input tree. is degree of node t. Then, the automaton proceeds by selecting a tuple from set and splitting into copies of itself. For each , one copy enters into state and proceeds to the node . This process produces a run over a tree.

Formally, a run on the input tree satisfy following two conditions:

  1. For every with , there exists a such that for every , we have and

Acceptance condition[edit]

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. The interesting accepting conditions are Büchi, Rabin, Streett and Muller. If for an input -labeled tree there exist an accepting run then the input tree is accepted by the automaton. The set of all the accepted -labeled trees is called tree language which is recognized by tree automaton .


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 , , and transition relation has exactly one element. Otherwise the automaton is non-deterministic.

Accepting tree languages[edit]

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.[2]

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

Reference list[edit]

  1. ^ Rabin, M. O.: Decidability of second order theories and automata on infinite trees,Transactions of the American Mathematical Society, vol. 141, pp. 1–35, 1969.
  2. ^ Rabin, M. O.: Weakly definable relations and special automata,Mathematical logic and foundation of set theory, pp. 1–23, 1970.