A Comparison of BDD-Based Parity Game Solvers

TL;DR

This paper evaluates and compares the performance of four BDD-based algorithms for solving parity games, which are crucial in verification and synthesis, across various random and benchmark game instances.

Contribution

It provides an empirical comparison of four BDD-based parity game solvers, highlighting their relative efficiencies on different game types.

Findings

Priority Promotion algorithm outperforms others on certain benchmarks.

Zielonka's recursive algorithm shows strengths in specific game structures.

Automata-based APT algorithm demonstrates competitive performance in large games.

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.