Game Development Reference

In-Depth Information

and a positional strategy (
W, S
)itcan

be decided in polynomial time, whether the strategy is winning on
W
.To

decide winning regions we can therefore just guess winning strategies, and

verify them in polynomial time.

Hence, given a finite parity game

G

Corollary 4.3
Winning regions of parity games (on finite game graphs)

can be decided in
NP

∩

Co-NP
.

Co-UP,

where UP denotes the class of NP-problems with unique witnesses. The

best known deterministic algorithm has complexity
n
O
(
√
n
)
) (Jurdzinski et al.

[2006]). For parity games with a number
d
of priorities the progress measure

lifting algorithm by Jurdzinski [2000] computes winning regions in time

O
(
dm

In fact, Jurdzinski [1998] proved that the problem is in UP

∩

(2
n/
(
d/
2))
d/
2
)=
O
(
n
d/
2+
O
(1)
), where
m
is the number of edges,

giving a polynomial-time algorithm when
d
is bounded. The two approaches

can be combined to achieve a worst-case running time of
O
(
n
n/
3+
O
(1)
) for

solving parity games with
d
priorities. These, and other, algorithms, are

explained in detail in Jurdzinski's contribution to this topic.

·

4.3 Reachability games and logic

We now discuss connections between logic and games for the special case of

reachability games. We assume that the reader is familiar with first-order

logic.

(1) Computing winning regions of reachability games is equivalent, under

very simple reductions, to computing minimal models for propositional

Horn formulae.

(2) The model-checking games for first-order logic are reachability games.

We will then discuss the definability problem for winning regions of reach-

ability games and see that more powerful formalisms than first-order logic

are needed.

4.3.1 Games and Horn formulae

Recall that a
propositional Horn formula
is a conjunction of implication

clauses of the form
Z

X
k
where
X
1
,...X
k
are propositional

variables, forming the
body
of the clause, and
Z
, the
head
of the clause, is

either also a propositional variable, or the constant 0. Notice that the body

of the clause can also be empty, in which case the clause takes the form

←

X
1
∧···∧

Search Nedrilad ::

Custom Search