Predicting Winning Regions in Parity Games via Graph Neural Networks (Extended Abstract)

TL;DR

This paper introduces a novel incomplete polynomial-time method using graph neural networks to predict winning regions in parity games, demonstrating practical effectiveness with 60% accuracy on a large dataset.

Contribution

The paper presents the first application of graph neural networks to approximate solutions for parity games, offering a practical approach with polynomial-time complexity.

Findings

Correctly predicts winning regions in ~60% of test games

Achieves high efficiency and practical effectiveness

Minor errors observed in remaining cases

Abstract

Solving parity games is a major building block for numerous applications in reactive program verification and synthesis. While they can be solved efficiently in practice, no known approach has a polynomial worst-case runtime complexity. We present a incomplete polynomial-time approach to determining the winning regions of parity games via graph neural networks. Our evaluation on 900 randomly generated parity games shows that this approach is effective and efficient in practice. It correctly determines the winning regions of $\sim$60\% of the games in our data set and only incurs minor errors in the remaining ones. We believe that this approach can be extended to efficiently solve parity games as well.