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.
Contents
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
Run
A run of tree automaton
Formally, a run
-
r ( ϵ ) = q 0 - For every
t ∈ T r r ( t ) = q , there exists a( q 1 , . . . , q d ( t ) ) ∈ δ ( q , V ( t ) , d ( t ) ) such that for every0 < i ≤ d ( t ) , we havet . i ∈ T r r ( t . i ) = q i
Acceptance condition
In a run
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
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.