Computer Science Logic and 8th Kurt Gödel Colloquium Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski: Simple stochastic parity games

Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print this page 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 one-player games, respectively, with turn-based 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)$. © 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04