University of Twente Student Theses


Formalization of tangle and tangle learning algorithm

Christiano, B.G. (2022) Formalization of tangle and tangle learning algorithm.

[img] PDF
Abstract:A parity game is an infinite duration game played on a directed graph by two players with each node labeled with a certain natural number. Both players move a token along the edges of the graph and the winner of a game depends on the parity of the highest labeled number of the nodes occurring infinitely often in a path of the token's movement. Parity game is involved in many formal verification problems such as automaton synthesis and verification, and bounded model checking. Solving a parity game is the process of computing the winner of a parity game; various algorithms have been created for this purpose and one of them, the tangle learning algorithm, is of interest in this research. A proof of the algorithm's correctness written in pen-and-paper has been given and this research defines and proves several underlying concepts involved in the algorithm in Isabelle, a software for interactive theorem proving. Isabelle provides a generic approach in verification of specifications or properties of software and algorithms defined as mathematical theorems. Formal proofs are written in a formal system and mechanically verifiable which makes them more accurate, reliable, and easier to verify. First, we define and prove several underlying theoretical concepts involved in the algorithm, then we give a partial implementation of the algorithm in Isabelle.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page