University of Twente Student Theses
Groovy Parity Games
Kooij, D. (2019) Groovy Parity Games.
|
PDF
413kB |
| 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: | https://purl.utwente.nl/essays/78707 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page