Game Development Reference
In-Depth Information
b
t ( ε )= b
t (0) = a
t (01) = b
a
b
t (110) = a
b
b
b
b
a a
a a
b a
a a
.
Figure 2.9 The initial part of an infinite tree over the alphabet
{
a, b
}
2.4 Tree automata
Infinite trees are a useful tool to model the behaviour of discrete systems
(circuits, protocols, etc.). These can be described by transition graphs, and
the possible behaviours or executions of such a system are captured by an
infinite tree: the unravelling of the transition graph. Properties of the system
behaviour can thus be specified as properties of infinite trees.
For simplicity we restrict ourselves to complete binary trees. The nodes
are labelled by symbols from a finite alphabet Σ. When modelling system
executions by infinite trees this alphabet captures properties of the system
we are interested in.
Formally, a tree is a mapping t :
}
Σ. The root of the tree
corresponds to the empty string ε . For some node u
{
0 , 1
} the left
successor is u 0, and the right successor is u 1. This is illustrated in
Figure 2.9 showing the initial part of a tree over the alphabet
∈{
0 , 1
. The
name of a node corresponds to the sequence of left (0) and right (1) moves
that lead to this node from the root.
We now introduce an automaton model that defines sets (languages) of
such infinite trees. This model can be seen as an extension of ω -automata to
trees, and it is also an extension of the model of automata on finite trees. As
for ω -automata, one can study different models that are distinguished by the
form of their acceptance condition. We focus here on parity tree automata,
which are defined as follows.
A parity tree automaton (PTA) is of the form
{
a, b
}
=( Q, Σ ,q in , Δ , pri )
with a finite set Q of states, a label alphabet Σ, an initial state q in ,a
transition relation Δ
A
Q
×
Σ
×
Q
×
Q , and a priority function pri : Q
N
.
}
Q (a Q -
labelled tree) that starts in the initial state, ρ ( ε )= q in , and that respects
A run ρ of a PTA on a tree t is a mapping ρ :
{
0 , 1