high performance computing on graphics processing units: hgpu.org

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.