Paper: Benchmarking Parity Games

Update 26 May 2015: Slides added.

Next week, on April 24, I will present my paper Benchmarking Parity Games at FSEN 2015. The core contribution of this paper is a set of parity games that can be used for benchmarking purposes.

Background

While working on my PhD thesis, 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.

Contribution

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.

Concluding remarks

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 (e.g. at ), 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?

Further reading

An extended version of the paper is available as J. J. A. Keiren. Benchmarks for Parity Games. arXiv.org [cs.LO] No. 1407.3121. 2014.

Links

  • 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 is available from the servers of the Open University in the Netherlands, you can download 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.

Slides

PhD dissertation

After four years of hard work, I defended my PhD thesis, of which the summary is included below, on 17 September. I experienced the day of the defence as a great day. It was very nice to see so many of my family, friends and colleagues. Thank you!

Summary

Advanced Reduction Techniques for Model Checking

Cover_Front_smallModern-day software systems are highly complex, and typically consist of a number of in- teracting components running in parallel. Verification methods aim to prove correctness of such systems. Model checking is a commonly used verification technique, in which a model of the system under investigation is created. Subsequently, it is checked whether this model satisfies certain properties.

Model checking suffers from the infamous state space explosion problem: the number of states in a system grows exponentially in the number of parallel components. Part of the blow-up is also due to the presence of data in descriptions of model checking problems. Typically model checkers construct the full state space, causing the approach to break down already for a small number of parallel components. Properties are then checked on the state space, either directly, or by first combining the state space with a property, leading to, for example, a Boolean equation system or a parity game. The latter step leads to a further blow up.

In this thesis techniques are developed to counter this state space explosion problem in (parameterised) Boolean equation systems and parity games. The main contributions are as follows:

  • A structural operational semantics is presented that can equip Boolean equation systems with arbitrary right hand sides with a graph structure, called structure graph. Classical graph structures for analysing Boolean equation systems typically restrict right hand sides to purely conjunctive or disjunctive form, essentially redu- cing the equation system to a parity game. We use our graphs to study the effects of this restriction on right hand sides, and show that, in the context of bisimulation, this reduction never poses a disadvantage.
  • We investigate the reductions that can be achieved using strong bisimulation reduction of structure graphs, and we investigate idempotence identifying bisimulation. We show that, although it indeed identifies idempotence in a restricted subset of equation systems, it does not live up to its name for full-blown structure graphs.
  • The insights we gain by studying structure graphs motivate further investigation of weaker equivalences in the setting of parity games. Since the winner in parity games is determined by the infinitely often recurring priorities, intuitively, finite stretches of similar vertices can be compressed. We define the notions of stuttering equivalence and governed stuttering equivalence, and show that they preserve the winner in a parity game.
  • A new set of benchmarks for parity games is developed due to the unavailability of standard benchmarks. These benchmarks subsume the examples that are used for performance evaluation of solving algorithms in the literature. We provide a description of the benchmarks, and we analyse their characteristics.The efficacy of our equivalences for reducing parity games is evaluated using this set of benchmarks. It is shown that large reductions are possible, even reducing parity games to a single vertex with a self-loop. Average reductions of about 50% are achieved. Sometimes the technique allows solving parity games which cannot be solved directly; in general, however, the timing results do not show a clear advantage.
  • Finally, we move from a posteriori reduction of parity games, to static analysis tech- niques for parameterised Boolean equation systems, that allow the a priori reduc- tion of the induced parity games. Essentially, we present a heuristic that performs a live variable analysis. We show that this analysis is more effective at reducing the complexity than existing techniques, i.e. the reductions that we obtain are larger. Correctness of our analysis is shown using a generalisation of the equivalences that we introduced for parity games and Boolean equation systems.