Infinite tree automaton
Encyclopedia
In computer science
and mathematical logic
, an infinite tree automaton is a state machine that deals with infinite tree structure. 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 automaton.
-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,
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:
, 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 Buchi, 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 
.
Infinite tree automaton is deterministic if for some
, 
, and 
transition relation 
has exactly one element. Otherwise the automaton is non-deterministic.
But, Buchi accepting condition is strictly weaker than other accepting contitions, 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 buchi accepting condition in some infinite tree automaton.
Tree languages which are recognized by muller accepting conditions are closed under union, intersection, projection and complementation.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
and mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, an infinite tree automaton is a state machine that deals with infinite tree structure. It can be viewed as an extension from a finite tree automaton
Tree automaton
A tree automaton is a type of state machine. Tree automata deal with tree structures, rather than the strings of more conventional state machines.The following article deals with branching tree automata, which correspond to regular languages of trees...
, 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
Büchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
and the Muller automaton
Muller automaton
In automata theory, a Muller automaton is a type of an ω-automaton.The acceptance condition separates a Muller automomaton from other ω-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 automaton.
Definition
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.
Run
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:
-
- For every
with 
, there exists a 
such that for every 
, we have 
and 
Acceptance condition
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 Buchi, 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 .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
, , and transition relation has exactly one element. Otherwise the automaton is non-deterministic.Accepting tree languages
Muller, parity, Rabin, and Streett accepting conditions in a infinite tree automaton recognize the same tree languages.But, Buchi accepting condition is strictly weaker than other accepting contitions, 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 buchi accepting condition in some infinite tree automaton.
Tree languages which are recognized by muller accepting conditions are closed under union, intersection, projection and complementation.