Symbolic Parity Game Solvers that Yield Winning Strategies

TL;DR

This paper introduces two new symbolic algorithms for solving parity games that can produce winning strategies, addressing the scalability issue in LTL synthesis by leveraging BDDs and demonstrating competitive performance.

Contribution

The paper presents the first symbolic parity game algorithms capable of yielding winning strategies, based on recent fixpoint methods, and evaluates their effectiveness empirically.

Findings

Algorithms are competitive with existing methods.

They can produce winning strategies efficiently.

Performance evaluated on SYNTCOMP 2020 benchmarks.

Abstract

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.