University of Twente Student Theses
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.
|
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 |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page