Finding Smaller Parity Game Solutions by Identifying and Solving Subgames using Oink

Solving parity games is an important step in some reactive synthesis tools. Reactive synthesis is the process of synthesising a controller that implements a formal definition. Finding smaller solutions to parity games can lead to smaller controller designs. Decreasing the size of controllers improves their efficiency. We propose an algorithm that identifies subgames of parity games to find smaller solutions. We implement subgame identification by building on the tool Oink and discover how it benefits performance. We compare multiple approaches to the problem and we show that pruning algorithms are a more viable approach to finding subgames than growing algorithms. We also compare the quality-based performance of various solvers to get a better understanding of the tool Oink.