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.
|
PDF
868kB |
| 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: | https://purl.utwente.nl/essays/98665 |
| 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