A Comparison of BDD-Based Parity Game Solvers
arXiv:1809.03097 · doi:10.4204/EPTCS.277.8
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.
arXiv commentIn Proceedings GandALF 2018, arXiv:1809.02416
References in corpus (7)
- Succinct progress measures for solving parity games
- Oink: an Implementation and Evaluation of Modern Parity Game Solvers
- Benchmarks for Parity Games (extended version)
- The Fixpoint-Iteration Algorithm for Parity Games
- Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds
- Generating and Solving Symbolic Parity Games
- A Delayed Promotion Policy for Parity Games