[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space

  • SPIN 2017
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Parity games play an important role in model checking and synthesis. In their paper, Calude et al. have recently shown that these games can be solved in quasi-polynomial time. We show that their algorithm can be implemented efficiently: we use their data structure as a progress measure, allowing for a backward implementation instead of a complete unravelling of the game. To achieve this, a number of changes have to be made to their techniques, where the main one is to add power to the antagonistic player that allows for determining her rational move without changing the outcome of the game. We provide a first implementation for a quasi-polynomial algorithm, test it on small examples, and provide a number of side results, including minor algorithmic improvements, a quasi-bi-linear complexity in the number of states and edges for a fixed number of colours, matching lower bounds for the algorithm of Calude et al., and a complexity index associated to our approach, which we compare to the recently proposed register index.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3

Similar content being viewed by others

Notes

  1. We recall Definition 1, which state when rules 1 and 2 are defined to be applied.

References

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

    Article  MathSciNet  MATH  Google Scholar 

  2. Ash, R.B.: Information Theory. Dover Publications Inc., New York (1990)

    MATH  Google Scholar 

  3. Berwanger, D., Dawar, A., Hunter, P., Kreutzer, S.: Dag-width and parity games. In: Proceedings of STACS, pp. 524–436. Springer, Berlin (2006)

  4. Björklund, H., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Appl. Math. 155(2), 210–229 (2007). https://doi.org/10.1016/j.dam.2006.04.029

    Article  MathSciNet  MATH  Google Scholar 

  5. Browne, A., Clarke, E.M., Jha, S., Long, D.E., Marrero, W.: An improved algorithm for the evaluation of fixpoint expressions. TCS 178(1–2), 237–255 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  6. Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, pp. 252–263. ACM (2017)

  7. Chatterjee, K., Henzinger, M., Loitzenbauer, V.: Improved algorithms for one-pair and k-pair streett objectives. In: Proceedings of LICS, pp. 269–280. IEEE Computer Society (2015)

  8. de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: Proceedings of LICS, pp. 279–290 (2001)

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

  10. Emerson, E.A., Jutla, C.S.: Tree automata, \(\mu \)-calculus and determinacy. In: Proceedings of FOCS, pp. 368–377. IEEE Computer Society Press (1991)

  11. Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional \(\mu \)-calculus. In: Proceedings of LICS, pp. 267–278. IEEE Computer Society Press (1986)

  12. Fearnley, J., Jain, S., Schewe, S., Stephan, F., Wojtczak, D.: An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10–14, 2017, pp. 112–121. ACM (2017)

  13. Fearnley, J.: Non-oblivious strategy improvement. In: Proceedings of LPAR, pp. 212–230 (2010)

  14. Friedmann, O., Lange, M.: PGSolver version 4.0 (2017). https://github.com/tcsprojects/pgsolver

  15. Friedmann, O., Lange, M.: Solving parity games in practice. In: Proceedings of ATVA, pp. 182–196 (2009)

  16. Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. University of Munich (2014). http://www.win.tue.nl/~timw/downloads/amc2014/pgsolver.pdf

  17. Friedmann, O.: An exponential lower bound for the latest deterministic strategy iteration algorithms. LMCS 7(3) (2011)

  18. Friedmann, O.: Recursive algorithm for parity games requires exponential time. RAIRO-Theor. Inf. Appl. 45(4), 449–457 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  19. Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: Proceedings of CAV, LNCS, vol. 9780, pp. 291–311 (2016)

  20. Jurdziński, M., Lazić, R.: Succinct progress measures for solving parity games. In: Proceedings of LICS 2017, p. (to appear) (2017). arXiv:1702.05051

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

  22. Jurdziński, M.: Small progress measures for solving parity games. In: Proceedings of STACS, pp. 290–301. Springer, Berlin (2000)

  23. Jurdziński, M.: Deciding the winner in parity games is in UP \(\cap \) co-UP. Inf. Process. Lett. 68(3), 119–124 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  24. Kozen, D.: Results on the propositional \(\mu \)-calculus. TCS 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  25. Lange, M.: Solving parity games by a reduction to SAT. In: Proceedings of International Workshop on Games in Design and Verification (2005)

  26. Lehtinen, K.: A modal \(\mu \) perspective on solving parity games in quasi-polynomial time. To appear in the proceedings of LiCS’18

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  29. Obdržálek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Proceedings of CAV, pp. 80–92. Springer, Berlin (2003)

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

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

  32. Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Proceedings of LOPSTR, pp. 127–142. Springer, Berlin (2006)

  33. Schewe, S., Finkbeiner, B.: The alternating-time \(\mu \)-calculus and automata over concurrent game structures. In: Proceedings of CSL, pp. 591–605. Springer, Berlin (2006)

  34. Schewe, S., Trivedi, A., Varghese, T.: Symmetric strategy improvement. In: Proceedings of ICALP, LNCS, vol. 9135, pp. 388–400 (2015)

  35. Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Proceedings of CSL 2008, pp. 368–383. Springer, Berlin (2008)

  36. Schewe, S.: Solving parity games in big steps. J. Comput. Syst. Sci. 84, 243–262 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  37. Totzke, P.: Implementation of the succinct progress measures algorithm from [22] (2017). https://github.com/pazz/pgsolver/tree/sspm

  38. Vardi, M.Y.: Reasoning about the past with two-way automata. In: Proceedings of ICALP, pp. 628–641. Springer, Berlin (1998)

  39. Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games. In: Proceedings of the CAV, pp. 202–215. Springer, Berlin (2000)

  40. Wilke, T.: Alternating tree automata, parity games, and modal \(\mu \)-calculus. Bull. Soc. Math. Belg. 8(2), 359 (2001)

    MathSciNet  MATH  Google Scholar 

  41. 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  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

We thank Xiang Fei Ding for pointing out an error in a previous version of this manuscript. We thank Tin Lok Wong for help with programming and implementation of the algorithms. We thank anonymous reviewers for many helpful suggestions and improvements made to a preliminary submission of this manuscript. Sanjay Jain was supported in part by NUS Grant C252-000-087-001. Further, Sanjay Jain and Frank Stephan were supported in part by the Singapore Ministry of Education Academic Research Fund Tier 2 Grant MOE2016-T2-1-019 / R146-000-234-112. Sven Schewe and Dominik Wojtczak were supported in part by EPSRC Grant EP/M027287/1. Further, John Fearnley, Bart de Keijzer, Sven Schewe and Dominik Wojtczak were supported in part by EPSRC Grant EP/P020909/1.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Liverpool, Liverpool, UK

    John Fearnley, Sven Schewe & Dominik Wojtczak

  2. Department of Computer Science, School of Computing, National University of Singapore, Singapore, Singapore

    Sanjay Jain & Frank Stephan

  3. Department of Computer Science and Electronic Engineering, University of Essex, Colchester, UK

    Bart de Keijzer

  4. Department of Mathematics, National University of Singapore, Singapore, Singapore

    Frank Stephan

Authors
  1. John Fearnley
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sanjay Jain
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bart de Keijzer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sven Schewe
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Frank Stephan
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Dominik Wojtczak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bart de Keijzer.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Fearnley, J., Jain, S., de Keijzer, B. et al. An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. Int J Softw Tools Technol Transfer 21, 325–349 (2019). https://doi.org/10.1007/s10009-019-00509-3

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-019-00509-3

Keywords

Search

Navigation