Paper: Benchmarking Parity Games
Next week, on April 24, I will present my paper Benchmarking Parity Games (missing reference) at FSEN 2015. The core contribution of this paper is a set of parity games that can be used for benchmarking purposes.
While working on my PhD thesis (missing reference), and several papers on parity games that are part of it, I observed that papers in the literature that discuss parity game algorithms take one of the following approaches:
- the paper focuses on the theoretical complexity of the algorithm.
- the paper describes an experimental evaluation of an algorithm, but uses a limited set of parity games for this evaluation.
An additional observation for the second category of papers is that each paper defines its own set of parity games to do this evaluation. If we want to compare experimental results, for instance because we want to see whether our own algorithm or heuristic is an improvement compared to an existing algorithm, it is problematic that we cannot do so based on a standard set of games.
In this paper, I provide a set of parity games that can be used to overcome the problem illustrated above. The set consists of games representing different problems: synthetic games, i.e. random games and families of games that are hard for some existing algorithms; model checking games; equivalence checking games; and games for satisfiability and validity of modal logics.
Additionally, I describe an analysis of the games with respect to a set of structural properties, including a newly developed notion of alternation depth for parity games. This new notion is an attempt to more accurately describe the inherent complexity of a parity game, along the same lines as the different notions of alternation depth that exist for the modal mu-calculus. Details can be found in the paper.
Currently the set of benchmarks does not include parity games generated from synthesis problems; such games would form a very welcome addition. If you would like to contribute such games (or any other games) please contact me, I would be more than happy to include them.
The analysis of the benchmarks that is described in the paper also gives rise to some interesting research questions:
- Can structural properties of graphs be computed more efficiently (especially width measures of graphs could not be computed for reasonably sized instances)?
- Are there heuristics that can approximate the graph measures that cannot be computed exactly?
- Can the theoretical complexity of parity game algorithms be improved by considering the notion of alternation depth that I propose?
An extended version of the paper is available as (missing reference)
- Parity game generator GitHub repository. This is the code I used to generate the parity games. For instructions see the ReadMe in the repository.
- PGInfo GitHub repository. This is the tool that I created to determine the structural information of the parity games.
- The generated games, and the corresponding data are available on Figshare. This includes the following:
- Model checking: Parity games encoding model checking problems.
- Equivalence checking: Parity games encoding equivalence checking problems.
- PGSolver: Parity games generated using PGSolver. These include: random games, and games that are hard for certain algorithms.
- MLSolver: Parity games generated using MLSolver. These are games that encode satisfiability and validity problems for modal logics.
- Data (YAML): This is a file in YAML format that includes high-level information about all parity games described before. Detailed (structural) information about the games can be found as separate YAML files in the respectipe ZIP archives.
- Data (SQLite): This contains a database in SQLite format that was derived from the YAML files provided in the archives, and the previous data file. The sole purpose of this derived data is to enable efficient plotting of results. The plots in the paper have been based on this file.
Contributions to the tools and the sets of games are appreciated.