Skip to main content

An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games

  • Conference paper
Computer Science Logic (CSL 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5213))

Included in the following conference series:

Abstract

This paper presents a novel strategy improvement algorithm for parity and payoff games, which is guaranteed to select, in each improvement step, an optimal combination of local strategy modifications. Current strategy improvement methods stepwise improve the strategy of one player with respect to some ranking function, using an algorithm with two distinct phases: They first choose a modification to the strategy of one player from a list of locally profitable changes, and subsequently evaluate the modified strategy. This separation is unfortunate, because current strategy improvement algorithms have no effective means to predict the global effect of the individual local modifications beyond classifying them as profitable, adversarial, or stale. Furthermore, they are completely blind towards the cross effect of different modifications: Applying one profitable modification may render all other profitable modifications adversarial. Our new construction overcomes the traditional separation between choosing and evaluating the modification to the strategy. It thus improves over current strategy improvement algorithms by providing the optimal improvement in every step, selecting the best combination of local updates from a superset of all profitable and stale changes.

This work was partly supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 109.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 139.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Kozen, D.: Results on the propositional μ-calculus. Theor. Comput. Sci. 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  2. Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of μ-calculus. In: Proc. CAV, pp. 385–396 (1993)

    Google Scholar 

  3. Wilke, T.: Alternating tree automata, parity games, and modal μ-calculus. Bull. Soc. Math. Belg. 8(2) (2001)

    Google Scholar 

  4. de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: Dynamic programs for omega-regular objectives. In: Proc. LICS, pp. 279–290. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  5. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  6. Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. Schewe, S., Finkbeiner, B.: The alternating-time μ-calculus and automata over concurrent game structures. In: Proc. CSL, pp. 591–605. Springer, Heidelberg (2006)

    Google Scholar 

  8. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: Proc. LICS, pp. 255–264. IEEE Computer Society, Los Alamitos (2006)

    Google Scholar 

  9. Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 127–142. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Emerson, E.A., Lei, C.: Efcient model checking in fragments of the propositional μ-calculus. In: Proc. LICS, pp. 267–278. IEEE Computer Society Press, Los Alamitos (1986)

    Google Scholar 

  11. Emerson, E.A., Jutla, C.S.: Tree automata, μ-calculus and determinacy. In: Proc. FOCS, pp. 368–377. IEEE Computer Society Press, Los Alamitos (1991)

    Google Scholar 

  12. McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  13. Zwick, U., Paterson, M.S.: The complexity of mean payoff games on graphs. Theoretical Computer Science 158(1–2), 343–359 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  14. 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)

    Article  MATH  MathSciNet  Google Scholar 

  15. Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1-2), 135–183 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Ludwig, W.: A subexponential randomized algorithm for the simple stochastic game problem. Inf. Comput. 117(1), 151–155 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  18. Puri, A.: Theory of hybrid systems and discrete event systems. PhD thesis, Computer Science Department, University of California, Berkeley (1995)

    Google Scholar 

  19. Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games. In: Proc. CAV, pp. 202–215. Springer, Heidelberg (2000)

    Google Scholar 

  20. Björklund, H., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Appl. Math. 155(2), 210–229 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  21. Obdržálek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80–92. Springer, Heidelberg (2003)

    Google Scholar 

  22. Lange, M.: Solving parity games by a reduction to SAT. In: Proc. Int. Workshop on Games in Design and Verification (2005)

    Google Scholar 

  23. Berwanger, D., Dawar, A., Hunter, P., Kreutzer, S.: Dag-width and parity games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 524–536. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: Proc. SODA, pp. 117–123. ACM/SIAM (2006)

    Google Scholar 

  25. Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 449–460. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Takaoka, T.: Theory of 2-3 heaps. In: Asano, T., Imai, H., Lee, D.T., Nakano, S.-i., Tokuyama, T. (eds.) COCOON 1999. LNCS, vol. 1627, pp. 41–50. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  27. Schewe, S.: Synthesis of Distributed Systems. PhD thesis, Saarland University, Saarbrücken, Germany (2008)

    Google Scholar 

  28. Smale, S.: On the average number of steps of the simplex method of linear programming. Mathematical Programming 27(3), 241–262 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  29. Klee, F., Minty, G.J.: How good is the simplex algorithm? Inequalities III, pp. 159–175 (1972)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Michael Kaminski Simone Martini

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schewe, S. (2008). An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games. In: Kaminski, M., Martini, S. (eds) Computer Science Logic. CSL 2008. Lecture Notes in Computer Science, vol 5213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-87531-4_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-87530-7

  • Online ISBN: 978-3-540-87531-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics