University of Twente Student Theses
Formalization of tangle and tangle learning algorithm
Christiano, B.G. (2022) Formalization of tangle and tangle learning algorithm.
|
PDF
523kB |
| 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: | https://purl.utwente.nl/essays/92054 |
| 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