nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Efficient Parallel Strategy Improvement for Parity Games

verfasst von : John Fearnley

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We study strategy improvement algorithms for solving parity games. While these algorithms are known to solve parity games using a very small number of iterations, experimental studies have found that a high step complexity causes them to perform poorly in practice. In this paper we seek to address this situation. Every iteration of the algorithm must compute a best response, and while the standard way of doing this uses the Bellman-Ford algorithm, we give experimental results that show that one-player strategy improvement significantly outperforms this technique in practice. We then study the best way to implement one-player strategy improvement, and we develop an efficient parallel algorithm for carrying out this task, by reducing the problem to computing prefix sums on a linked list. We report experimental results for these algorithms, and we find that a GPU implementation of this algorithm shows a significant speedup over single-core and multi-core CPU implementations.

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 SMTCoq: A Plug-In for Integrating SMT Solvers into Coq

Nächstes Kapitel Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems

This is because the algorithm requires that every vertex has a distinct priority, and so comparing two valuations requires O(n) time.

https://github.com/jfearnley/parallel-si.

Hoffman, A.J., Karp, R.M.: On nonterminating stochastic games. Manag. Sci. 12(5), 359–370 (1966)MathSciNetCrossRefMATH

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

Cochet-Terrasson, J., Gaubert, S.: Policy iteration algorithm for shortest path problems. Technical report (2000)

Cole, R., Vishkin, U.: Faster optimal parallel prefix sums and list ranking. Inf. Comput. 81(3), 334–352 (1989)MathSciNetCrossRefMATH

Condon, A.: On algorithms for simple stochastic games. In: Proceedings of a DIMACS Workshop, Advances in Computational Complexity Theory, pp. 51–72 (1990)

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

Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of \(\mu \)-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_32 CrossRef

Fearnley, J., Savani, R.: The complexity of all-switches strategy improvement. In: Proceedings of SODA, pp. 130–139 (2016)

Friedmann, O.: An exponential lower bound for the latest deterministic strategy iteration algorithms. Log. Methods Comput. Sci. 7(3) (2011). Paper 23. http://www.lmcs-online.org/ojs/viewarticle.php?id=779&layout=abstract

10.

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). doi:10.1007/978-3-642-04761-9_15 CrossRef

11.

Grädel, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002)MATH

12.

Helman, D.R., JáJá, J.: Designing practical efficient algorithms for symmetric multiprocessors. In: Goodrich, M.T., McGeoch, C.C. (eds.) ALENEX 1999. LNCS, vol. 1619, pp. 37–56. Springer, Heidelberg (1999). doi:10.1007/3-540-48518-X_3 CrossRef

13.

Hoffmann, P., Luttenberger, M.: Solving parity games on the GPU. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 455–459. Springer, Cham (2013). doi:10.1007/978-3-319-02444-8_34 CrossRef

14.

Huth, M., Kuo, J.H.-P., Piterman, N.: Concurrent small progress measures. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 130–144. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34188-5_13 CrossRef

15.

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

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). doi:10.1007/3-540-46541-3_24 CrossRef

17.

Kandziora, J.: Playing parity games on the playstation 3. In: Twente Student Conference (2009)

18.

Keiren, J.J.A.: Benchmarks for parity games. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 127–142. Springer, Cham (2015). doi:10.1007/978-3-319-24644-4_9 CrossRef

19.

Ladner, R.E., Fischer, M.J.: Parallel prefix computation. J. ACM 27(4), 831–838 (1980)MathSciNetCrossRefMATH

20.

Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games. CoRR, abs/0806.2923 (2008)

21.

Matoušek, J., Sharir, M., Welzl, E.: A subexponential bound for linear programming. Algorithmica 16(4–5), 498–516 (1996)MathSciNetCrossRefMATH

22.

Meyer, P.J., Luttenberger, M.: Solving mean-payoff games on the GPU. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 262–267. Springer, Cham (2016). doi:10.1007/978-3-319-46520-3_17 CrossRef

23.

Mostowski, A.W.: Games with forbidden positions. Technical report 78, University of Gdańsk (1991)

24.

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

25.

Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (2005)MATH

26.

Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 369–384. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87531-4_27 CrossRef

27.

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). doi:10.1007/3-540-60218-6_1 CrossRef

28.

van de Pol, J., Weber, M.: A multi-core solver for parity games. Electr. Notes Theoret. Comput. Sci. 220(2), 19–34 (2008)CrossRefMATH

29.

van der Berg, F.: Solving parity games on the playstation 3. In: Twente Student Conference (2010)

30.

Vöge, J., Jurdziński, 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). doi:10.1007/10722167_18 CrossRef

31.

Wei, Z., JáJá, J.: Optimization of linked list prefix computations on multithreaded GPUs using CUDA. Parallel Process. Lett. 22(4), 1250012 (2012)MathSciNetCrossRef

32.

Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci. 200, 135–183 (1998)MathSciNetCrossRefMATH

33.

Zwick, U., Paterson, M.S.: The complexity of mean payoff games on graphs. Theoret. Comput. Sci. 158(1–2), 343–359 (1996)MathSciNetCrossRefMATH

Titel: Efficient Parallel Strategy Improvement for Parity Games
verfasst von: John Fearnley
Verlag: Springer International Publishing
Buch: Computer Aided Verification
Print ISBN: 978-3-319-63389-3

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

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-63390-9_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"