A matrix-based approach to parity games

Saksham Aggarwal, Alejandro Stuckey De La Banda, Luke Yang, Julian Gutierrez

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review


Parity games are two-player zero-sum games of infinite duration played on finite graphs for which no solution in polynomial time is still known. Solving a parity game is an NP∩co-NP problem, with the best worst-case complexity algorithms available in the literature running in quasi-polynomial time. Given the importance of parity games within automated formal verification, several practical solutions have been explored showing that considerably large parity games can be solved somewhat efficiently. Here, we propose a new approach to solving parity games guided by the efficient manipulation of a suitable matrix-based representation of the games. Our results show that a sequential implementation of our approach offers very competitive performance, while a parallel implementation using GPUs outperforms the current state-of-the-art techniques. Our study considers both real-world benchmarks of structured games as well as parity games randomly generated. We also show that our matrix-based approach retains the optimal complexity bounds of the best recursive algorithm to solve large parity games in practice.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication29th International Conference, TACAS 2023 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 Paris, France, April 22–27, 2023 Proceedings, Part I
EditorsSriram Sankaranarayanan, Natasha Sharygina
Place of PublicationCham Switzerland
Number of pages18
ISBN (Electronic)9783031308239
ISBN (Print)9783031308222
Publication statusPublished - 2023
EventTools and Algorithms for the Construction and Analysis of Systems 2023 - Paris, France
Duration: 22 Apr 202327 Apr 2023
https://link.springer.com/book/10.1007/978-3-031-30823-9 (Proceedings)
https://etaps.org/2023/conferences/ (Website)

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceTools and Algorithms for the Construction and Analysis of Systems 2023
Abbreviated titleTACAS 2023
Internet address


  • Parity game
  • Formal verification
  • Parallel computing

Cite this