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