University of Twente Student Theses
Solving Parity Games: Combining Progress Measures and Tangle Learning
Stekelenburg, A.V. (2024) Solving Parity Games: Combining Progress Measures and Tangle Learning.
|
PDF
2MB |
| Abstract: | An oft-used method for verifying the correctness of software is model checking. One technique for performing model checking involves converting a model and specification into a parity game and solving this parity game to obtain information about the model. There are many algorithms for solving parity games. Most of these run in exponential time, but recently some were found which run in quasi-polynomial time. Most of these quasi-polynomial algorithms are from the family of progress measure-based algorithms. However, these algorithms tend to be impractically slow on large games. On the other hand, there are the attractor-based algorithms which tend to be fast in practice but have an exponential time complexity. In this thesis we present an algorithm which accelerates the value iteration of any progress measure by using attractors. We prove the correctness of this algorithm and some of its variants. To do this we first establish a set of requirements on what makes a suitable progress measure. Finally, we perform some empirical performance tests and an analysis of the complexity of the algorithm which show that the algorithm significantly accelerates the progress measure algorithms while having a time complexity that is equivalent to the progress measure that is used. |
| 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/98019 |
| 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