Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Components as Location Graphs Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Solving Parity Games in Scala

verfasst von : Antonio Di Stasio, Aniello Murano, Vincenzo Prignano, Loredana Sorrentino

Erschienen in: Formal Aspects of Component Software

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Formal Rules for Reliable Component-Based Architecture Evolution
Nächstes Kapitel Synthesis of a Reconfiguration Service for Mixed-Criticality Multi-Core Systems: An Experience Report
Literatur
1.
Aminof, B., Mogavero, F., Murano, A.: Synthesis of hierarchical systems. Sci. Comp. Program. 83, 56–79 (2013)CrossRef
2.
Antonik, A., Charlton, N., Huth, M.: Polynomial-time under-approximation of winning regions in parity games. ENTCS 225, 115–139 (2009)
3.
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)CrossRef
5.
Berger, E.D., Zorn, B.G., McKinley, K.S.: Composing high-performance memory allocators. ACM SIGPLAN Not. 36, 114–124 (2001)CrossRef
6.
Berger, E.D., Zorn, B.G., McKinley, K.S.: OOPSLA 2002: reconsidering custom memory allocation. ACM SIGPLAN Not. 48(4), 46–57 (2013)CrossRef
7.
Berwanger, D.: Admissibility in infinite games. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 188–199. Springer, Heidelberg (2007)CrossRef
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)
9.
Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS’05, pp. 178–187 (2005)
10.
Chatterjee, K., Jurdzinski, M., Henzinger, T.A.: Quantitative stochastic parity games. In: SODA’04, pp. 121–130 (2004)
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)CrossRef
12.
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2002)
13.
Emerson, E., Jutla, C.: Tree automata, \(\mu \)-calculus and determinacy. In: FOCS’91, pp. 368–377 (1991)
14.
Friedmann, O.: Recursive algorithm for parity games requires exponential time. RAIRO-Theor. Inform. Appl. 45(04), 449–457 (2011)CrossRefMATHMathSciNet
15.
Friedmann, O., Lange, M.: The pgsolver collection of parity game solvers. University of Munich (2009)
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)CrossRef
17.
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Pearson Education, New Jersey (1994)
18.
Gay, D., Aiken, A.: Memory management with explicit regions. ACM Sigplan Not. 33, 313–323 (1998)CrossRef
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)CrossRef
20.
Hundt, R.: Loop recognition in c++/java/go/scala. In: 2011 Proceedings of Scala Days (2011)
21.
Jurdzinski, M.: Deciding the winner in parity games is in up \(\cap \) co-up. Inf. Process. Lett. 68(3), 119–124 (1998)CrossRefMathSciNet
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)CrossRef
23.
Jurdzinski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comput. 38(4), 1519–1532 (2008)CrossRefMATHMathSciNet
24.
25.
Kupferman, O., Vardi, M., Wolper, P.: An automata theoretic approach to branching-time model checking. JACM 47(2), 312–360 (2000)CrossRefMATHMathSciNet
26.
27.
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)CrossRef
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)
30.
Odersky, M., Spoon, L., Venners, B.: Programming in Scala. Artima Inc, Sunnyvale (2008)
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)CrossRef
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)CrossRef
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)
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)CrossRef
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)CrossRefMATHMathSciNet
Metadaten
Titel
Solving Parity Games in Scala
verfasst von
Antonio Di Stasio
Aniello Murano
Vincenzo Prignano
Loredana Sorrentino
Copyright-Jahr
2015
Buch
Formal Aspects of Component Software

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

Electronic ISBN: 978-3-319-15317-9

Copyright-Jahr: 2015

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