A Multi-Core Solver for Parity Games

Jan Cornelis van de Pol; M. Weber

doi:10.1016/j.entcs.2008.11.011

A Multi-Core Solver for Parity Games

Jan Cornelis van de Pol, M. Weber

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

12 Citations (Scopus)

108 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)
Editors	I. Černá, G. Lüttgen
Place of Publication	Amsterdam
Publisher	Elsevier
Pages	19-34
Number of pages	14
DOIs	https://doi.org/10.1016/j.entcs.2008.11.011
Publication status	Published - 29 Mar 2008
Event	7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008 - Budapest, Hungary Duration: 29 Mar 2008 → 29 Mar 2008 Conference number: 7 http://anna.fi.muni.cz/PDMC/PDMC08/cfp.shtml

Publication series

Name	Electronic Notes in Theoretical Computer Science
Publisher	Elsevier
Number	2
Volume	220
ISSN (Print)	1571-0661
ISSN (Electronic)	1571-0661

Workshop

Workshop	7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008
Abbreviated title	PDMC
Country/Territory	Hungary
City	Budapest
Period	29/03/08 → 29/03/08
Internet address	http://anna.fi.muni.cz/PDMC/PDMC08/cfp.shtml

Keywords

IR-64838
METIS-254876
EWI-12953

Access to Document

10.1016/j.entcs.2008.11.011

main

Cite this

@inproceedings{1755e2e1fbb24d40872033d624e459c9,

title = "A Multi-Core Solver for Parity Games",

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.",

keywords = "IR-64838, METIS-254876, EWI-12953",

author = "{van de Pol}, {Jan Cornelis} and M. Weber",

year = "2008",

month = mar,

day = "29",

doi = "10.1016/j.entcs.2008.11.011",

language = "English",

series = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier",

number = "2",

pages = "19--34",

editor = "I. {\v C}ern{\'a} and G. L{\"u}ttgen",

booktitle = "Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)",

address = "Netherlands",

note = "7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008, PDMC ; Conference date: 29-03-2008 Through 29-03-2008",

url = "http://anna.fi.muni.cz/PDMC/PDMC08/cfp.shtml",

}

van de Pol, JC & Weber, M 2008, A Multi-Core Solver for Parity Games. in I Černá & G Lüttgen (eds), Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008). Electronic Notes in Theoretical Computer Science, no. 2, vol. 220, Elsevier, Amsterdam, pp. 19-34, 7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008, Budapest, Hungary, 29/03/08. https://doi.org/10.1016/j.entcs.2008.11.011

A Multi-Core Solver for Parity Games. / van de Pol, Jan Cornelis; Weber, M.
Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008). ed. / I. Černá; G. Lüttgen. Amsterdam: Elsevier, 2008. p. 19-34 (Electronic Notes in Theoretical Computer Science; Vol. 220, No. 2).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Multi-Core Solver for Parity Games

AU - van de Pol, Jan Cornelis

AU - Weber, M.

N1 - Conference code: 7

PY - 2008/3/29

Y1 - 2008/3/29

N2 - 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.

AB - 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.

KW - IR-64838

KW - METIS-254876

KW - EWI-12953

U2 - 10.1016/j.entcs.2008.11.011

DO - 10.1016/j.entcs.2008.11.011

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 19

EP - 34

BT - Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)

A2 - Černá, I.

A2 - Lüttgen, G.

PB - Elsevier

CY - Amsterdam

T2 - 7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008

Y2 - 29 March 2008 through 29 March 2008

ER -

A Multi-Core Solver for Parity Games

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this