A Multi-Core Solver for Parity Games

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)
    40 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 languageEnglish
    Title of host publicationProceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)
    EditorsI. Černá, G. Lüttgen
    Place of PublicationAmsterdam
    PublisherElsevier
    Pages19-34
    Number of pages14
    DOIs
    Publication statusPublished - 29 Mar 2008
    Event7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008 - Budapest, Hungary
    Duration: 29 Mar 200829 Mar 2008
    Conference number: 7
    http://anna.fi.muni.cz/PDMC/PDMC08/cfp.shtml

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    PublisherElsevier
    Number2
    Volume220
    ISSN (Print)1571-0661
    ISSN (Electronic)1571-0661

    Workshop

    Workshop7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008
    Abbreviated titlePDMC
    CountryHungary
    CityBudapest
    Period29/03/0829/03/08
    Internet address

    Fingerprint

    Model checking
    Parallel algorithms
    Network protocols
    Data storage equipment

    Keywords

    • IR-64838
    • METIS-254876
    • EWI-12953

    Cite this

    van de Pol, J. C., & 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) (pp. 19-34). (Electronic Notes in Theoretical Computer Science; Vol. 220, No. 2). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2008.11.011
    van de Pol, Jan Cornelis ; Weber, M. / A Multi-Core Solver for Parity Games. Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008). editor / I. Černá ; G. Lüttgen. Amsterdam : Elsevier, 2008. pp. 19-34 (Electronic Notes in Theoretical Computer Science; 2).
    @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 = "3",
    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. Čern{\'a} and G. L{\"u}ttgen",
    booktitle = "Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)",

    }

    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 proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - A Multi-Core Solver for Parity Games

    AU - van de Pol, Jan Cornelis

    AU - Weber, M.

    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

    ER -

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