A Multi-Core Solver for Parity Games

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

    10 Citations (Scopus)
    57 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

    Keywords

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

    Fingerprint Dive into the research topics of 'A Multi-Core Solver for Parity Games'. Together they form a unique fingerprint.

  • 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