A Multi-Core Solver for Parity Games


Pol, Jaco van de and Weber, Michael (2008) A Multi-Core Solver for Parity Games. Electronic Notes in Theoretical Computer Science, 220 (2). pp. 19-34. ISSN 1571-0661

open access
Abstract:We describe a parallel algorithm for solving parity games,
with applications in, e.g., modal mu-calculus model
checking with arbitrary alternations, and (branching) bisimulation
checking. The algorithm is based on Jurdzinski's Small Progress
Measures. Actually, this is a class of algorithms, depending on
a selection heuristics.

Our algorithm operates lock-free, and mostly wait-free (except for
infrequent termination detection), and thus allows maximum
parallelism. Additionally, we conserve memory by avoiding storage
of predecessor edges for the parity graph through strictly
forward-looking heuristics.

We evaluate our multi-core implementation's behaviour on parity games
obtained from mu-calculus model checking problems for a set of
communication protocols, randomly generated problem instances, and
parametric problem instances from the literature.

Item Type:Article
Copyright:© 2008 Elsevier
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/64838
Official URL:https://doi.org/10.1016/j.entcs.2008.11.011
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 254876