University of Twente Student Theses


A Formal Proof for the Correctness of Tangle Learning

Veen, S.E. van der (2024) A Formal Proof for the Correctness of Tangle Learning.

[img] PDF
Abstract:Parity games are a type of two-player game that have applications in model checking. Scientifically, they are interesting because their complexity indicates that they might be solved in polynomial time, but no algorithm capable of solving them in polynomial time has been discovered as of yet. Tangle learning is one algorithm that aims to solve parity games, which has a correctness proof on paper, but no computer-verified proof. This thesis focuses on a correctness proof of tangle learning using the Isabelle/HOL interactive theorem prover, with the aim of improving confidence in the correctness of the algorithm and exploring how such proofs can be done. We first define basic concepts of parity games and prove important properties thereof. Then, we give definitions for concepts related to tangle learning. We define our tangle attractor algorithm and the search algorithm, one of two algorithms that together constitute tangle learning, using inductive predicates for step relations of loops. We then prove the correctness of our tangle attractor algorithm and finally prove that the search algorithm finds a finite set of tangles that is nonempty if its input region is nonempty, and that search terminates. We have not completed the correctness proof of solve, the second algorithm that is part of tangle learning.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page