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
Corollary 4.3 Winning regions of parity games (on finite game graphs)
can be decided in NP
Co-NP .
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
(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