Skip to main content
SpringerLink
Log in

Solving Parity Games in Scala

  • Conference paper
  • First Online:
Book cover Formal Aspects of Component Software (FACS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8997))

Included in the following conference series:

Abstract

Parity games are two-player games, played on directed graphs, whose nodes are labeled with priorities. Along a play, the maximal priority occurring infinitely often determines the winner. In the last two decades, a variety of algorithms and successive optimizations have been proposed. The majority of them have been implemented in PGSolver, written in OCaml, which has been elected by the community as the de facto platform to solve efficiently parity games as well as evaluate their performance in several specific cases.

PGSolver includes the Zielonka Recursive Algorithm that has been shown to perform better than the others in randomly generated games. However, even for arenas with a few thousand of nodes (especially over dense graphs), it requires minutes to solve the corresponding game.

In this paper, we deeply revisit the implementation of the recursive algorithm introducing several improvements and making use of Scala Programming Language. These choices have been proved to be very successful, gaining up to two orders of magnitude in running time.

Aniello Murano—Partially supported by the FP7 European Union project 600958-SHERPA and OR.C.HE.S.T.R.A. MIUR PON project.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
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

References

  1. Aminof, B., Mogavero, F., Murano, A.: Synthesis of hierarchical systems. Sci. Comp. Program. 83, 56–79 (2013)

    Article  Google Scholar 

  2. Antonik, A., Charlton, N., Huth, M.: Polynomial-time under-approximation of winning regions in parity games. ENTCS 225, 115–139 (2009)

    Google Scholar 

  3. Aminof, B., Kupferman, O., Murano, A.: Improved model checking of hierarchical systems. Inf. Comput. 210, 68–86 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  4. Barringer, H., Havelund, K.: TraceContract: a scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57–72. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Berger, E.D., Zorn, B.G., McKinley, K.S.: Composing high-performance memory allocators. ACM SIGPLAN Not. 36, 114–124 (2001)

    Article  Google Scholar 

  6. Berger, E.D., Zorn, B.G., McKinley, K.S.: OOPSLA 2002: reconsidering custom memory allocation. ACM SIGPLAN Not. 48(4), 46–57 (2013)

    Article  Google Scholar 

  7. Berwanger, D.: Admissibility in infinite games. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 188–199. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Generalized mean-payoff and energy games. In: FSTTCS’10, LIPIcs 8, pp. 505–516 (2010)

    Google Scholar 

  9. Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS’05, pp. 178–187 (2005)

    Google Scholar 

  10. Chatterjee, K., Jurdzinski, M., Henzinger, T.A.: Quantitative stochastic parity games. In: SODA’04, pp. 121–130 (2004)

    Google Scholar 

  11. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  12. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2002)

    Google Scholar 

  13. Emerson, E., Jutla, C.: Tree automata, \(\mu \)-calculus and determinacy. In: FOCS’91, pp. 368–377 (1991)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  15. Friedmann, O., Lange, M.: The pgsolver collection of parity game solvers. University of Munich (2009)

    Google Scholar 

  16. Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182–196. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Pearson Education, New Jersey (1994)

    Google Scholar 

  18. Gay, D., Aiken, A.: Memory management with explicit regions. ACM Sigplan Not. 33, 313–323 (1998)

    Article  Google Scholar 

  19. Hoffmann, P., Luttenberger, M.: Solving parity games on the GPU. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 455–459. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  20. Hundt, R.: Loop recognition in c++/java/go/scala. In: 2011 Proceedings of Scala Days (2011)

    Google Scholar 

  21. Jurdzinski, M.: Deciding the winner in parity games is in up \(\cap \) co-up. Inf. Process. Lett. 68(3), 119–124 (1998)

    Article  MathSciNet  Google Scholar 

  22. 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 

  23. Jurdzinski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comput. 38(4), 1519–1532 (2008)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  25. Kupferman, O., Vardi, M., Wolper, P.: An automata theoretic approach to branching-time model checking. JACM 47(2), 312–360 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  26. Kupferman, O., Vardi, M., Wolper, P.: Module checking. IC 164(2), 322–344 (2001)

    MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  28. Mogavero, F., Murano, A., Sorrentino, L.: On promptness in parity games. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 601–618. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  29. Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An overview of the scala programming language (2004)

    Google Scholar 

  30. Odersky, M., Spoon, L., Venners, B.: Programming in Scala. Artima Inc, Sunnyvale (2008)

    Google Scholar 

  31. Queille, J., Sifakis, J.: Specification and verification of concurrent programs in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  32. 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 

  33. Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. MIT Press, Cambridge (1990)

    Google Scholar 

  34. Vöge, J., Jurdzinski, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  35. 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 

Download references

Author information

Authors and Affiliations

  1. Università degli Studi di Napoli Federico II, Napoli, Italy

    Antonio Di Stasio, Aniello Murano, Vincenzo Prignano & Loredana Sorrentino

Authors
  1. Antonio Di Stasio
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aniello Murano
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vincenzo Prignano
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Loredana Sorrentino
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Aniello Murano .

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, University of bologna, Bologna, Italy and Inria Sophia Antipolis - Méditerranée, Sophia Antipolis, France

    Ivan Lanese

  2. Inria Sophia Antipolis - Méditerranée, Sophia Antipolis, France

    Eric Madelaine

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Di Stasio, A., Murano, A., Prignano, V., Sorrentino, L. (2015). Solving Parity Games in Scala. In: Lanese, I., Madelaine, E. (eds) Formal Aspects of Component Software. FACS 2014. Lecture Notes in Computer Science(), vol 8997. Springer, Cham. https://doi.org/10.1007/978-3-319-15317-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-15317-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-15316-2

  • Online ISBN: 978-3-319-15317-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation