|title:||Termination of Zielonka|
|keywords:||Isabelle, Parity Games|
|topics:||Algorithms and Data Structures|
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 Isabelle/HOL.