University of Twente Student Theses

Login

A Formal Proof of the Termination of Zielonka's Algorithm for Solving Parity Games

Abraham, Remco (2019) A Formal Proof of the Termination of Zielonka's Algorithm for Solving Parity Games.

[img] PDF
148kB
Abstract:It is currently unknown whether parity games can be solved in polynomial time. Still, it is known that many problems related to model-checking and synthesis can be reduced to parity games. Algorithms that solve parity games are therefore of great value. One of the earliest algorithms invented for this purpose is the algorithm proposed by Zielonka. Various pen and paper proofs of its correctness have been provided, but although parity games play an important role in many machine-generated and machine verified proofs, Zielonka's algorithm has no machine-checked proof itself. As a starting point for the formal proof of Zielonka's algorithm, this research will provide a formal proof for the termination of the algorithm using the formal theorem prover Isabelle/HOL.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:31 mathematics, 54 computer science
Programme:Computer Science BSc (56964)
Link to this item:https://purl.utwente.nl/essays/78694
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page