Symbolic Parity Game Solvers that Yield Winning Strategies

Oebele Lijzenga, Tom van Dijk

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

83 Downloads (Pure)


Parity games play an important role for LTL synthesis as evidenced by recent breakthroughs on LTL synthesis, which rely in part on parity game solving. Yet state space explosion remains a major issue if we want to scale to larger systems or specifications. In order to combat this problem, we need to investigate symbolic methods such as BDDs, which have been successful in the past to tackle exponentially large systems. It is therefore essential to have symbolic parity game solving algorithms, operating using BDDs, that are fast and that can produce the winning strategies used to synthesize the controller in LTL synthesis.
Current symbolic parity game solving algorithms do not yield winning strategies. We now propose two symbolic algorithms that yield winning strategies, based on two recently proposed fixpoint algorithms. We implement the algorithms and empirically evaluate them using benchmarks obtained from SYNTCOMP 2020. Our conclusion is that the algorithms are competitive with or faster than an
earlier symbolic implementation of Zielonka’s recursive algorithm, while also providing the winning strategies.
Original languageEnglish
Title of host publicationProceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification
Subtitle of host publicationBrussels, Belgium, September 21-22, 2020
EditorsJean-Francois Raskin, Davide Bresolin
Place of PublicationWaterloo, NSW
PublisherOpen Publishing Association
Publication statusPublished - 22 Sept 2020
Event11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020 - Online
Duration: 21 Sept 202023 Sept 2020
Conference number: 11

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
ISSN (Electronic)2075-2180


Conference11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020
Abbreviated titleGandALF
Internet address


Dive into the research topics of 'Symbolic Parity Game Solvers that Yield Winning Strategies'. Together they form a unique fingerprint.

Cite this