Game Development Reference

In-Depth Information

Section 2.5 we give an outlook beyond finite automata, and in Section 2.6

we conclude.

This chapter is written as a gentle introduction to the subject of infinite

games and automata theory. Many concepts, techniques, and proofs are

explained using examples without being formally rigorous. For the interested

reader who wants to learn more about the subject we give some pointers to

the literature in the conclusion.

2.2 Basic notations and definitions

For a set
X
we denote by
X
∗
the set of finite sequences and by
X
ω

the set

X
ω

of infinite sequences over
X
.For
α

∈

let

Inf(
α
)=
{x ∈ X | x
occurs infinitely often in
α}.

We can view an infinite sequence
α ∈ X
ω
as a mapping
α
: N
→ X
.

Consequently, we write
α
(
i
) to denote the element at position
i
in
α
, i.e.,

α
=
α
(0)
α
(1)
α
(2)

···

Infinite sequences are also called infinite words or
ω
-words.

A
game graph
(also called
arena
) is a tuple
G
=(
V
E
,V
A
,E,c
) with

•

V
E
: vertices of Eva (player 1, circle),

•

V
A
: vertices of Adam (player 2, box),

• E ⊆ V × V
: edges with
V
=
V
E
∪ V
A
,

• c
:
V → C
with a finite set of colours
C
.

The sets
V
E
and
V
A
are disjoint (each vertex belongs to exactly one of the

players). We are interested in plays of infinite duration played on such graphs.

Therefore, we assume that each vertex has at least one successor. Most of

the time we consider games on finite arenas but in Section 2.4 we also use

games on infinite graphs.

Example 2.1

Figure 2.1 shows a simple game graph with
V
E
=

{

x
1
,x
2

}

and
V
A
=

. We assume that
C
=
V
and that the colouring is the

identity function. Whenever we consider game graphs without specifying the

colouring, then we implicitly identify the vertices with the colours.

{

y
1
,y
2

}

A
play
in
G
is an infinite sequence
α
=
v
0
v
1
v
2
···

of vertices such that

(
v
i
,v
i
+1
)

∈

E
for all
i

≥

0. By
c
(
α
) we denote the corresponding sequence of

colours
c
(
v
0
)
c
(
v
1
)
c
(
v
2
)

···

A
game
is a pair of a game graph and a
winning condition
G

=(
G, Win
)

C
ω
. Eva wins a play
α
if
c
(
α
)

with
Win

⊆

∈

Win
. Otherwise Adam wins.

Search Nedrilad ::

Custom Search