Speeding up the small progress measures algorithm for parity games using the GPU

P.J.A. Bootsma
Eindhoven University of Technology
Eindhoven University of Technology, 2013


   title={Speeding up the small progress measures algorithm for parity games using the GPU},

   author={Bootsma, PJA and Willemse, TAC},



Download Download (PDF)   View View   Source Source   



Solving parity games is interesting because it is equivalent to model checking for mu-calculus. The small progress measures (SPM) algorithm by Jurdzinski is originally a sequential algorithm for solving parity games. The nature of this algorithm allows easy parallelization, and previous research has already adapted it to work on multi-core machines. Here, SPM is adapted to work on the many-core architecture used by modern graphics processing units (GPUs). Additionally, some existing techniques to speed up SPM or parity game solving in general are discussed, such as alternating SPM and simple graph preprocessing. A new technique is introduced that can help to reduces parity game solving times by assigning priorities to edges instead of vertices, after which shortcut edges can be added to the graph. Experimental validation shows that using the GPU for small progress measures can result in faster solving for some games, but the best solution is to let the CPU and GPU calculate in parallel and stop when either is done. Adding shortcuts when priorities are assigned to edges can also improve solving times for some games.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: