Game Development Reference

In-Depth Information

node labelled
b
is accepted by a PTA with two states
Q
=

, with

initial state
q
b
, priorities
pri
(
q
b
)=1,
pri
(
q
) = 2, and the transitions

{

q
b
,q

}

(
q
b
,a,q
b
,q
)
,
(
q
b
,a,q,q
b
)
,
(
q
b
,b,q,q
)
,
(
q, a, q, q
)
,
(
q, b, q, q
)
.

The state
q
b
is used to non-deterministically select a path that leads to

a node with label
b
. This is done by the first two transitions. A simple

argument shows that this language cannot be accepted by a deterministic

parity tree automaton.

We now analyse algorithmic and closure properties of PTAs. Some closure

properties are rather easy to obtain.

Proposition 2.13
The class of regular languages of infinite trees is closed

under union, intersection, and projection (relabelling).

Proof
For the closure under union and intersection one can use a classical

product construction where the two given automata are executed in parallel.

The acceptance condition becomes a Muller condition that expresses that

both automata accept for the intersection, or that at least one of the automata

accepts for the union. As mentioned above, one can use the LAR construction

to turn a Muller automaton into an equivalent parity automaton.

For the projection let
h
:Σ
→
Γ be a relabelling. It is applied to trees by

applying it to each label of the tree. Given a PTA
A
for a tree language
T

we want to construct a PTA for the tree language
h
(
T
)=
{h
(
t
)
| t ∈ T}
.

For this purpose we simply replace every transition (
q, a, q
0
,q
1
)in
A
by the

transition (
q, h
(
a
)
,q
0
,q
1
).

The connection to games is used for the closure under complementation

and the emptiness test, as explained in the following.

2.4.1 Complementation

Let us first analyse why the complementation problem for PTAs is a di
cult

problem. By definition, a tree is accepted if

∃

run

∀

path
.
(path satisfies acceptance condition)
.

By negation of this statement we obtain that a tree is not accepted if

∀

run

∃

path
.
(path does not satisfy acceptance condition)
.

This exchange of quantifiers makes the problem di
cult. But there are two

observations to make that lead towards the solution. First of all, statements

of the form

∃∀···

are very close to the nature of games and strategies: there

Search Nedrilad ::

Custom Search