Game Development Reference

In-Depth Information

determinised is of size

is of size

2
O
(
nk
log(
nk
))
. The construction presented by Muller and Schupp [1995] slightly

improves this to 2
O
(
nk
log(
n
))
.

As an application one can now use the closure properties of PTAs to show

their equivalence to monadic second-order logic over the infinite tree, i.e.,

over the structure (

O

(
nk
), and thus the resulting PTA

C

}
∗
and the

two successor relations
S
0
and
S
1
for moving left or right in the tree. As for

S1S the corresponding theory is referred to as S2S (second-order theory of

two successors). Again we abuse notation and also refer to the logic as S2S.

In analogy to the results for
ω
-automata and S1S presented in Section 2.3.3

we obtain the equivalence of S2S and tree automata.

}
∗
,S
0
,S
1
) consisting of the domain

{

0
,
1

{

0
,
1

n

is definable by an S2S formula iff it can be accepted by a parity tree automaton.

Theorem 2.17
(Rabin [1969])

A tree language L over the alphabet

{

0
,
1

}

If we want to check the satisfiability of S2S formulae, we can translate

them into tree automata and check these for emptiness. This latter problem

is the subject of the next section.

2.4.2 Emptiness

We now want to develop a method that checks for a given PTA

A

whether

) is empty or not. For the complementation construction we have used the

membership game to characterise the acceptance of a tree by the automaton.

The idea is that Constructor builds a run and Spoiler chooses a path

through this run. The resulting game arena is infinite because the moves

available at a certain node depend on the label of the tree at this node. For

the emptiness problem we want to know whether there is a tree on which

there is a run such that the acceptance condition is satisfied on each path:

T
(

A

∃

tree

∃

run

∀

path
.
(path satisfies acceptance condition)
.

Accordingly, we modify the membership game such that Constructor now

builds a tree
t
and a run
ρ
on
t
at the same time. This allows us to remove

the tree nodes from

}
∗
from the game positions because the moves do

not depend on these nodes anymore. This makes the game graph finite.

The
emptiness game
for a PTA
A
has the following rules:

{

0
,
1

•

The game positions are
Q

∪

Δ (states and transitions of

A

).

•

The initial position is
q
in
.

•

From a position
q
(a state of

) the game proceeds as follows:

1 Constructor picks a transition (
q, a, q
0
,q
1
),

A

Search Nedrilad ::

Custom Search