A comparison of BDD-based parity game solvers

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

4 Citations (Scopus)
2 Downloads (Pure)

Abstract

Parity games are two player games with omega-winning conditions, played on finite graphs. Such games play an important role in verification, satisfiability and synthesis. It is therefore important to identify algorithms that can efficiently deal with large games that arise from such applications. In this paper, we describe our experiments with BDD-based implementations of four parity game solving algorithms, viz. Zielonka's recursive algorithm, the more recent Priority Promotion algorithm, the Fixpoint-Iteration algorithm and the automata based APT algorithm. We compare their performance on several types of random games and on a number of cases taken from the Keiren benchmark set.

Original languageEnglish
Title of host publicationProceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification
Place of PublicationWaterloo
PublisherOpen Publishing Association
Pages103-117
Number of pages15
DOIs
Publication statusPublished - 7 Sep 2018
Event9th International Symposium on Games, Automata, Logics, and Formal Verification, G and ALF 2018 - Saarbrucken, Germany
Duration: 26 Sep 201828 Sep 2018

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume277

Conference

Conference9th International Symposium on Games, Automata, Logics, and Formal Verification, G and ALF 2018
Country/TerritoryGermany
CitySaarbrucken
Period26/09/1828/09/18

Fingerprint

Dive into the research topics of 'A comparison of BDD-based parity game solvers'. Together they form a unique fingerprint.

Cite this