Game Development Reference

In-Depth Information

function by setting its indicator set to:

Reach(
T
)=

{

v
0
,v
1
,v
2
,...

:
v
i
∈

T
for some
i

≥

0

}

.

Similarly, for a set of safe vertices
S

⊆

V
, we define the
safety payoff

function by setting its indicator set to:

Safe(
S
)=

{

v
0
,v
1
,v
2
,...

:
v
i
∈

S
for all
i

≥

0

}

.

Observe that Reach(
T
)=
V
ω

\

Safe(
V

\

T
). It implies that from a
reachabil-

ity game
with the target set
T

V
, by swapping the roles of players 0 and 1

and their payoff functions, we get a
safety game
with the safe set
V

⊆

\

T
,

and vice versa.

Given a set of target vertices
T

V
, we define the
repeated reachability

payoff
function, also referred to as
Buchi payoff
, by setting its indicator

set to:

⊆

Buchi(
T
)=
{v
0
,v
1
,v
2
,...
:
v
i
∈ T
for infinitely many
i ≥
0
},

and for a set
S

V
of safe vertices, we define the
eventual safety payoff

function, also known as
co-Buchi payoff
, function by setting its indicator

set to:

⊆

co-Buchi(
S
)=

{

v
0
,v
1
,v
2
,...

:
v
i

∈

S
for all but finitely many
i

≥

0

}

.

Again, the repeated reachability and eventual safety payoffs are dual in the

sense that from a repeated reachability game with a set of target vertices
T ⊆

V
, by swapping the roles of players 0 and 1 and their payoff functions, we get

an eventual safety game wit
h
the set of safe vertices
V

\

T
, and vice versa.

A
ω
, we define its
infinity

For a
n
infinite sequence
a
=

a
0
,a
1
,a
2
,...

∈

set
Inf(
a
)by:

Inf(
a
)=

{

a

∈

A
:
a
i
=
a
for infinitely many
i

≥

0

}

.

Note that the infinity set of every infinite sequence must be non-empty if the

set
A
is finite. For a
priority function
p
:
V →{
1
,
2
,...,d}
, we define

the
parity payoff
function by setting its indicator set to:

V
ω
: max Inf(

Parity(
p
)=

{

v
0
,v
1
,v
2
,...

∈

p
(
v
0
)
,p
(
v
1
)
,p
(
v
2
)
,...

)isodd

}

.

3.2 Solving repeated reachability and eventual safety games

The main results presented in this section are positional determinacy of

repeated reachability games and of eventual safety games, and a simple

divide-and-conquer algorithm
for solving them that runs in time
O
(
nm
).

Search Nedrilad ::

Custom Search