Abstract
We report on multi-core implementations of parity game solvers based on Small Progress Measures. We revisit a known implementation of multi-core machines (PW solver), and change, in what we call the PW e solver, the way it computes progress measures. We then suggest an alternative implementation (CSPM), that reduces logical dependency on configuration state and makes performance less dependent on configuration details. In experimental evaluation, both PW e and CSPM out-perform PW. On most benchmarks, especially larger ones, CSPM performs better than PW e . The observed linear speed-up of parallelization shows great promise for parallel implementations of game solvers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Etessami, K., Wilke, T., Schuller, R.A.: Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata. In: Yu, Y., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 694. Springer, Heidelberg (2001)
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)
Friedmann, O., Lange, M.: The pgsolver Collection of Parity Game Solvers. Technical report, Institut für Informatik, LMU Munich (February 2010) Version 3
Friedmann, O., Latte, M., Lange, M.: A Decision Procedure for CTL* Based on Tableaux and Automata. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 331–345. Springer, Heidelberg (2010)
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)
Jurdziński, M.: Deciding the winner in parity games is in UP∩co-UP. Inf. Process. Lett. 68, 119–124 (1998)
Kozen, D.: Results on the propositional μ-calculus. In: ICALP 1982, pp. 348–359 (1982)
Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Where’s waldo? sensor-based temporal logic motion planning. In: ICRA, pp. 3116–3121 (2007)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)
Stirling, C.: Local Model Checking Games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)
van de Pol, J., Weber, M.: A multi-core solver for parity games. In: PDMC. ENTCS, vol. 220(2), pp. 19–34 (2008)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huth, M., Kuo, J.HP., Piterman, N. (2012). Concurrent Small Progress Measures. In: Eder, K., Lourenço, J., Shehory, O. (eds) Hardware and Software: Verification and Testing. HVC 2011. Lecture Notes in Computer Science, vol 7261. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34188-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-34188-5_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34187-8
Online ISBN: 978-3-642-34188-5
eBook Packages: Computer ScienceComputer Science (R0)