Abstract
A discrete strategy improvement algorithm is given for constructing winning strategies in parity games, thereby providing also a new solution of the model-checking problem for the modal μ-calculus. Known strategy improvement algorithms, as proposed for stochastic games by Hoffman and Karp in 1966, and for discounted payoff games and parity games by Puri in 1995, work with real numbers and require solving linear programming instances involving high precision arithmetic. In the present algorithm for parity games these difficulties are avoided by the use of discrete vertex valuations in which information about the relevance of vertices and certain distances is coded. An efficient implementation is given for a strategy improvement step. Another advantage of the present approach is that it provides a better conceptual understanding and easier analysis of strategy improvement algorithms for parity games. However, so far it is not known whether the present algorithm works in polynomial time. The long standing problem whether parity games can be solved in polynomial time remains open.
Chapter PDF
Similar content being viewed by others
References
Browne, A., Clarke, E.M., Jha, S., Long, D.E., Marrero, W.: An improved algorithm for the evaluation of fixpoint expressions. Theoretical Computer Science 178(1-2), 237–255 (1997)
Buhrke, N., Lescow, H., Vöge, J.: Strategy construction in infinite games with Streett and Rabin chain winning conditions. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 27–29. Springer, Heidelberg (1996)
Condon, A.: The complexity of stochastic games. Information and Computation 96, 203–224 (1992)
Condon, A.: On algorithms for simple stochastic games. In: Cai, J.-Y. (ed.) Advances in Computational Complexity Theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 13, pp. 51–73. American Mathematical Society (1993)
Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. Journal of Game Theory 8(2), 109–113 (1979)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (Extended abstract). In: Proceedings of 32nd Annual Symposium on Foundations of Computer Science, pp. 368–377. IEEE Computer Society Press, Los Alamitos (1991)
Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of μ-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Hoffman, A., Karp, R.: On nonterminating stochastic games. Management Science 12, 359–370 (1966)
Jurdziński, M.: Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters 68(3), 119–124 (1998)
Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65(2), 149–184 (1993)
Megiddo, N.: Towards a genuinely polynomial algorithm for linear programming. SIAM Journal on Computing 12, 347–353 (1983)
Melekopoglou, M., Condon, A.: On the complexity of the policy improvement algorithm for stochastic games. ORSA (Op. Res. Soc. of America) Journal of Computing 6(2), 188–192 (1994)
Mostowski, A.W.: Games with forbidden positions. Technical Report 78, University of Gdańsk (1991)
Puri, A.: Theory of Hybrid Systems and Discrete Event Systems. PhD thesis, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, Memorandum No. UCB/ERL M95/113 (December 1995)
Schmitz, D., Vöge, J.: Implementation of a strategy improvement algorithm for finite-state parity games (April 2000) ( manuscipt, unpublished)
Seidl, H.: Fast and simple nested fixpoints. Information Processing Letters 59(6), 303–308 (1996)
Stirling, C.: Local model checking games (Extended abstract). In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)
Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games. Aachener Informatik-Berichte 2000-2, RWTH Aachen, Fachgruppe Informatik, 52056 Aachen, Germany (February 2000)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200, 135–183 (1998)
Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theoretical Computer Science 158, 343–359 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vöge, J., Jurdziński, M. (2000). A Discrete Strategy Improvement Algorithm for Solving Parity Games. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_18
Download citation
DOI: https://doi.org/10.1007/10722167_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive