Game Development Reference

In-Depth Information

functions of
ω
-regular
subsets of
Run
(
G
). The membership in an
ω
-regular

set of runs is determined by one of the
acceptance conditions
listed below.

These conditions correspond to acceptance criteria of finite-state automata

over infinite words (see Section 5.2.2 for more details).

•

Reachability and safety.
A run
w

∈

Run
(
G
) satisfies the
reachability

condition determined by a colour
c

∈

C
if
c

∈

ν
(
w
(
i
)) for some
i

≥

0. The

0.

•
Buchi and co-Buchi.
A run
w ∈ Run
(
G
) satisfies the
Buchi
condition

determined by a colour
c ∈ C
if
c ∈ ν
(
w
(
i
)) for infinitely many
i ≥
0. The

co-Buchi
condition is dual, i.e., there are only finitely many
i ≥
0 such

that
c ∈ ν
(
w
(
i
)).

safety
condition determined by
c
is dual, i.e.,
c

∈

ν
(
w
(
i
)) for all
i

≥

•

Rabin, Rabin-chain, and Street.
Let
Pairs
=

{

(
c
1
,d
1
)
,...,
(
c
m
,d
m
)

}

be a finite set of pairs of colours. A run
w

Run
(
G
) satisfies the
Rabin

condition determined by
Pairs
if there is (
c, d
)

∈

Pairs
such that
w

satisfies the Buchi condition determined by
d
and the co-Buchi condition

determined by
c
. The
Street
condition determined by
Pairs
is dual to

Rabin, i.e., for every (
c, d
)

∈

Pairs
we have that
w
satisfies the co-Buchi

condition determined by
d
or the Buchi condition determined by
c
.

For a given colour
c
, let
V
(
c
) be the set of all
v

∈

ν
(
v
).

The
Rabin-chain
(or
parity
) condition is a special case of the Rabin

condition where
Pairs
and
ν
satisfy
V
(
c
1
)

∈

V
such that
c

∈

⊂

V
(
d
1
)

⊂ ··· ⊂

V
(
c
m
)

⊂

V
(
d
m
).

•
Muller.
Let
M ⊆
2
C
be a set of subsets of colours. A run
w ∈ Run
(
G
)

satisfies the
Muller
condition determined by
M
if the set of all
c ∈ C
such

w
satisfies the Buchi condition determined by
c
is an element of
M
.

Let us note that
ω
-regular sets of runs are relatively simple in the sense that

they are contained in the first two levels of the Borel hierarchy (the sets of

runs satisfying the reachability and safety conditions are in the first level).

Quantitative payoffs

Quantitative payoff functions can capture more complicated properties of

runs that are particularly useful in performance and dependability analysis

of stochastic systems.

Let
r
:
V

be a bounded function which to every vertex
v
assigns the

reward
r
(
v
), which can be intuitively interpreted as a price paid by player

→
R

♦

to player

when visiting
v
. The limit properties of rewards that are paid

along a given run are captured by the following payoff functions:

•
Limit-average payoff
(also
mean-payoff
) assigns to each
w

∈

Run
(
G
)

Search Nedrilad ::

Custom Search