Symbolic parity games : Two novel fixpoint iteration algorithms with strategy derivation

In this paper, we study symbolic parity game solving using BDDs. The state of the art of symbolic parity game algorithms is improved by implementing two novel fixpoint iteration algorithms. Contrary to current symbolic algorithms, our algorithms also derive winning strategies. Empirical evaluation compares the new symbolic algorithms with a symbolic implementation of Zielonka's recursive algorithm over benchmark sets from SYNTCOMP 2020. We conclude that both new algorithms are competitive with Zielonka's algorithm, while also providing winning strategies.