University of Twente Student Theses
Explorations in Quasi-Polynomial Algorithms for Parity Games
Hol, V.R.L. (2025) Explorations in Quasi-Polynomial Algorithms for Parity Games.
|
PDF
607kB |
| Abstract: | Model checking and controller synthesis can be important techniques for ensuring the safety and long-term operation of complex systems. Both can rely on the translation of temporal logics into parity games, which can then be solved to address the original verification or synthesis problem. While parity games are widely believed to be solvable in polynomial time, no such algorithm has been discovered to date. The development of quasi-polynomial time (QPT) algorithms since 2017 has significantly improved the state of the art, with approaches ranging from progress measure-based and attractor-based algorithms to novel paradigms such as Lehtinen's register game algorithm. Lehtinen's algorithm in particular has not been implemented or benchmarked. We present explicit-state and symbolic-state algorithms for constructing register games. Additionally, a separate hybrid algorithm is proposed, combining an existing attractor-based QPT solver with memoization of tangles, a concept derived from Tangle Learning, to enhance performance. We establish the correctness of the hybrid algorithm and benchmark its performance, alongside Lehtinen's algorithm, demonstrating practical improvements in parity game solving when compared to the original QPT attractor-based algorithm. |
| 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/105231 |
| 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