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 ∧···∧