Game Development Reference
In-Depth Information
program then corresponds to a winning strategy for Eva. In Rosner [1991] it
is shown that the doubly exponential complexity is also a lower bound.
In a more general setting the synthesis problem has been posed by Church
[1962]. For the case of monadic second-order specifications it has been solved
by Buchi and Landweber [1969] as explained in the following.
We now consider monadic second-order logic over the natural numbers with
the successor function. Monadic second-order logic is the extension of first-
order logic by the ability to quantify over sets of elements. We do not give
the precise definition but only illustrate the syntax with an example. For a
more precise treatment of the subject we refer the reader to Thomas [1997].
The underlying structure (
, +1) consists of the natural numbers as domain
and the successor function. The corresponding theory, i.e., the sentences that
are true in (
N
, +1), is called the 'second-order theory of one successor' (S1S)
by Buchi [1962]. We slightly abuse the terminology here and also refer to the
logic itself as S1S.
We use small letters x, y, . . . as first-order variables denoting elements, and
capital letters X, Y, . . . for set variables denoting sets of natural numbers.
Consider the formula
N
Y 0
ϕ ( X )=
Y
x ( x
Y
x +1 /
Y )
Y ) .
It has one free set variable X denoting a set of natural numbers. We can
view a set of natural numbers as an ω -word over the alphabet
x ( x
X
x
{
0 , 1
}
by
labelling the positions in X by 1, and the other positions by 0.
Using this interpretation, ϕ defines the set of all ω -words over
such
that 1 can only occur on even positions: The formula states that there is a set
Y that contains position 0, and it contains exactly every second position (i.e.,
Y contains exactly the even positions), and it contains X . Thus, this formula
is true for each interpretation of the free variable X by a set containing only
even positions.
In general, we consider formulae ϕ ( X 1 ,...,X n )with n free set variables
defining ω -languages over
{
0 , 1
}
n . We have already seen that LTL formulae
(which also define languages over the alphabet
{
0 , 1
}
n ) can be translated
into automata. For S1S formulae we even have a stronger result that the two
formalisms are equivalent.
Theorem 2.11 (Buchi [1962])
{
0 , 1
}
n ) ω is definable by an
S1S formula iff it can be accepted by a non-deterministic Buchi automaton.
A language L
(
{
0 , 1
}