A comparison of BDD-based parity game solvers

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

2 Citaten (Scopus)
2 Downloads (Pure)

Samenvatting

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.

Originele taal-2Engels
TitelProceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification
Plaats van productieWaterloo
UitgeverijOpen Publishing Association
Pagina's103-117
Aantal pagina's15
DOI's
StatusGepubliceerd - 7 sep 2018
Evenement9th International Symposium on Games, Automata, Logics, and Formal Verification, G and ALF 2018 - Saarbrucken, Duitsland
Duur: 26 sep 201828 sep 2018

Publicatie series

NaamElectronic Proceedings in Theoretical Computer Science
Volume277

Congres

Congres9th International Symposium on Games, Automata, Logics, and Formal Verification, G and ALF 2018
LandDuitsland
StadSaarbrucken
Periode26/09/1828/09/18

Citeer dit

Sanchez, L., Wesselink, W., & Willemse, T. A. C. (2018). A comparison of BDD-based parity game solvers. In Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification (blz. 103-117). (Electronic Proceedings in Theoretical Computer Science ; Vol. 277). Open Publishing Association. https://doi.org/10.4204/EPTCS.277.8