Groovy Parity Games

Parity games are often used for the formal verification of software systems and for the μ-calculus model-checking problem, but reasoning about them is generally hard. Multiple algorithms solve parity games, but none of them do so in polynomial-time, even though it is widely believed that a polynomial algorithm exists. In this paper, we show that it is possible to model one such algorithm, priority promotion, as a series of graph transformations, and describe how to do it. Subsequently, we use these graph transformations to visualise the algorithm in the formal graph transformation tool Groove, with the goal to provide researchers with a better understanding of parity games. We also model several extensions to the algorithm using recursion and non-determinism. Finally, we reflect on the results and suggest directions for future research.