Quantitative stochastic parity games

ABSTRACT

We study perfect-information stochastic parity games. These are two-player nonterminating games which are played on a graph with turn-based probabilistic transitions. A play results in an infinite path and the conflicting goals of the two players are ω-regular path properties, formalized as parity winning conditions. The qualitative solution of such a game amounts to computing the set of vertices from which a player has a strategy to win with probability 1 (or with positive probability). The quantitative solution amounts to computing the value of the game in every vertex, i.e., the highest probability with which a player can guarantee satisfaction of his own objective in a play that starts from the vertex.For the important special case of one-player stochastic parity games (parity Markov decision processes) we give polynomial-time algorithms both for the qualitative and the quantitative solution. The running time of the qualitative solution is O(d · m^3/2) for graphs with m edges and d priorities. The quantitative solution is based on a linear-programming formulation.For the two-player case, we establish the existence of optimal pure memoryless strategies. This has several important ramifications. First, it implies that the values of the games are rational. This is in contrast to the concurrent stochastic parity games of de Alfaro et al.; there, values are in general algebraic numbers, optimal strategies do not exist, and ε-optimal strategies have to be mixed and with infinite memory. Second, the existence of optimal pure memoryless strategies together with the polynomial-time solution forone-player case implies that the quantitative two-player stochastic parity game problem is in NP ∩ co-NP. This generalizes a result of Condon for stochastic games with reachability objectives. It also constitutes an exponential improvement over the best previous algorithm, which is based on a doubly exponential procedure of de Alfaro and Majumdar for concurrent stochastic parity games and provides only ε-approximations of the values.

REFERENCES

• 1: A. Arnold and D. Niwiński. Rudiments of μ-Calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2001.
• 2: A. Arnold , A. Vincent , I. Walukiewicz, Games for synthesis of controllers with partial observation, Theoretical Computer Science, v.303 n.1, p.7-34, 28 June 2003 [doi>10.1016/S0304-3975(02)00442-5]
• 3: J. C. Bradfield, The modal mu-calculus alternation hierarchy is strict, Theoretical Computer Science, v.195 n.2, p.133-153, March 30, 1998 [doi>10.1016/S0304-3975(97)00217-X]
• 4: K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Simple stochastic parity games. In CSL'03, volume 2803 of LNCS, pages 100--113. Springer, 2003.
• 5: Anne Condon, The complexity of stochastic games, Information and Computation, v.96 n.2, p.203-224, Feb. 1992 [doi>10.1016/0890-5401(92)90048-K]
• 6: Costas Courcoubetis , Mihalis Yannakakis, Markov decision processes and regular events, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.336-349, July 1990, Warwick University, England
• 7: L. de Alfaro and T. A. Henzinger. Concurrent ω-regular games. In LICS'00, pages 141--154. IEEE Computer Society Press, 2000.
• 8: L. de Alfaro , T. A. Henzinger , O. Kupferman, Concurrent Reachability Games, Proceedings of the 39th Annual Symposium on Foundations of Computer Science, p.564, November 08-11, 1998
• 9: Luca de Alfaro , Rupak Majumdar, Quantitative solution of omega-regular games380872, Proceedings of the thirty-third annual ACM symposium on Theory of computing, p.675-683, July 2001, Hersonissos, Greece [doi>10.1145/380752.380871]
• 10: E. A. Emerson , C. S. Jutla, Tree automata, Mu-Calculus and determinacy, Proceedings of the 32nd annual symposium on Foundations of computer science, p.368-377, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 11: E. Allen Emerson , Charanjit S. Jutla , A. Prasad Sistla, On Model-Checking for Fragments of µ-Calculus, Proceedings of the 5th International Conference on Computer Aided Verification, p.385-396, June 28-July 01, 1993
• 12: H. Everett. Recursive games. In Contributions to the Theory of Games III, volume 39 of Annals of Mathematical Studies, pages 47--78. Princeton University Press, 1957.
• 13: Jerzy Filar , Koos Vrieze, Competitive Markov decision processes, Springer-Verlag New York, Inc., New York, NY, 1996
• 14: E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games. A Guide to Current Research, volume 2500 of LNCS. Springer, 2002.
• 15: Yuri Gurevich , Leo Harrington, Trees, automata, and games, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.60-65, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802177]
• 16: Marcin Jurdziński, Deciding the winner in parity games is in UP ∩ co-UP, Information Processing Letters, v.68 n.3, p.119-124, Nov. 15, 1998 [doi>10.1016/S0020-0190(98)00150-1]
• 17: Marcin Jurdzinski, Small Progress Measures for Solving Parity Games, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, p.290-301, February 01, 2000
• 18: M. L. Littman, T. Dean, and L. P. Kaelbling. On the complexity of solving Markov decision problems. In UAI'95, pages 394--402. Morgan Kaufmann, 1995.
• 19: D. A. Martin. The determinacy of Blackwell games. Journal of Symbolic Logic, 63(4):1565--1581, 1998.
• 20: Anuj Puri, Theory of hybrid systems and discrete event systems, University of California at Berkeley, Berkeley, CA, 1996
• 21: Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons, Inc., New York, NY, 1994
• 22: T. E. S. Raghavan and J. A. Filar. Algorithms for stochastic games --- a survey. ZOR --- Methods and Models of Operations Research, 35:437--472, 1991.
• 23: L. S. Shapley. Stochastic games. Proceedings Nat. Acad. of Science USA, 39:1095--1100, 1953.
• 24: A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley and Los Angeles, 1951.
• 25: Wolfgang Thomas, Languages, automata, and logic, Handbook of formal languages, vol. 3: beyond words, Springer-Verlag New York, Inc., New York, NY, 1997
• 26: Jens Vöge , Marcin Jurdzinski, A Discrete Strategy Improvement Algorithm for Solving Parity Games, Proceedings of the 12th International Conference on Computer Aided Verification, p.202-215, July 15-19, 2000
• 27: J. von Neumann and O. Morgenstern. Theory of Games and Economic Behavior. Princeton University Press, 1953.
• 28: Wiesław Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theoretical Computer Science, v.200 n.1-2, p.135-183, June 28, 1998 [doi>10.1016/S0304-3975(98)00009-7]
• 29: Uri Zwick , Mike Paterson, The complexity of mean payoff games on graphs, Theoretical Computer Science, v.158 n.1-2, p.343-359, May 20, 1996 [doi>10.1016/0304-3975(95)00188-3]