author: Remco Abraham
title: Termination of Zielonka
keywords: Isabelle, Parity Games
topics: Algorithms and Data Structures
started: April 2019
end: July 2019


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.