Predicting Winning Regions in Parity Games via Graph Neural Networks

Abstract

Parity games are two-player games that are a fundamental model for reactive systems, with applications in program verification and synthesis. Solving parity games is known to be in the complexity class UP \cap coUP, making it challenging to solve e!ciently in the worst-case scenario. This work extends previous research that aimed to tackle the computational complexity of parity games. The previous work did so by proposing a novel approach utilizing Graph Neural Network for solving parity games e!ciently. The results suggest that this approach with graph neural networks has the potential to provide e!cient and accurate solutions to parity games, with the model correctly predicting ⇡ 60% of the winning regions. In this thesis, we experimentally evaluate the performance of the initial graph neural network solver against classical methods and existing solvers. On the basis of this evaluation, we propose a new model that correctly predicts ⇡ 90% of the winning regions, achieves a speed up of up to 2.5, and a minimal memory usage reduction of 93%.