Solving parity games is a major building block for numerous applications in reactive program verification and synthesis. While there exist efficient approaches to solving parity games in practice, none of these have a polynomial worst-case runtime complexity. We present a incomplete 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 efficient in practice. It moreover correctly determines the winning regions of ~60% of the games in our data set and only incurs minor errors in the remaining ones.
翻译:解决平价游戏是反应性程序验证和合成中众多应用的主要基石。 虽然在实际中存在解决平价游戏的有效方法, 但其中没有一个是多式最坏的运行时间复杂度。 我们提出一个不完整的方法来通过图形神经网络确定平价游戏的赢家区域。 我们对900个随机生成的平价游戏的评估表明,这个方法在实践中是有效的。 此外,它正确地确定了我们数据集中60%的赢家区域,而在其余的游戏中,只有很小的错误。