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 ).