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.

Monadic second-order logic

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

}

Search Nedrilad ::

Custom Search