Abstract

The aim of this thesis is to investigate how parity game problems may be solved efficiently in practice. Parity games are a worthwhile research topic because their simultaneous simplicity and expressiveness makes them a useful formalism to represent the problems that occur when formal methods are applied to software and hardware engineering.

In this thesis, first an overview of the state of the art, both theoretical and practical, will be presented. Second, algorithms and data structures will be described which were used to develop a new parity game solving tool. These include a mix of well-known, relative obscure, previously undocumented, and completely novel techniques. The most valuable contributions are the introduction of novel preprocessing operations and improved heuristics for the Small Progress Measures solution algorithm. Third, the results of an empirical evaluation will be presented to demonstrate which of these techniques work best in practice.

The empirical results will support the conclusion that considerable improvements over the state of the art are possible using a combination of careful tool design and implementation, application of powerful preprocessing operations, and the use of ad- vanced heuristics in the implementation of the Small Progress Measures algorithm.

Additional Resources

1. The paper