University of Twente Student Theses


Groovy Parity Games

Kooij, D. (2019) Groovy Parity Games.

[img] PDF
Abstract: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.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Awards:Best Paper Award
Keywords:Parity games, Priority promotion, Visualisation, Attractor computation, Formal verication, μ-calculus, Model checking, Graph transformations, Groove, Control program, State space exploration, Non-determinism, Recursion
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page