Game Development Reference
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
• 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 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
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 )