
Many verification, planning, and control problems can be modelled as games played on state/transition graphs by one or two players whose conflicting goals are to form a path in the graph satisfying a given qualitative objective or a quantitative optimal reward objective. Such games and their subclasses have been extensively, and often independently, studied in several research communities, such as stochastic games, Markov decision processes (MDP), temporal model checking, and AI planning. The focus here is on simple stochastic parity games and MDP's, i.e., two and oneplayer games, respectively, with turnbased probabilistic transitions and fairness objectives formalized as the parity (Rabin chain) winning condition.
An efficient translation is given from simple stochastic parity games and parity MDP's to simple parity games. As many algorithms are known for the latter the translation yields efficient algorithms for qualitative solution of simple stochastic parity games and MDP's.
Another main result is a novel subquadratic algorithm for qualitative solution of MDP's with reachability and B\"uchi objectives: it works in time $O(n \sqrt{n})$ compared with $O(n^2)$ for best previously known algorithms. Interestingly, a similar technique sheds light on the important question of the computational complexity of solving simple B\"uchi games yielding the first provably subquadratic algorithm for the problem with running time $O(n^2/ \log n)$.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 