A symmetric attractor-decomposition lifting algorithm for parity games

TL;DR

This paper introduces a symmetric attractor-decomposition lifting algorithm for parity games that improves upon existing quasi-polynomial algorithms by overcoming asymmetry limitations and unifying different approaches.

Contribution

It develops a symmetric lifting algorithm that accelerates both players' strategies and unifies various quasi-polynomial algorithms for solving parity games.

Findings

The symmetric algorithm matches the worst-case performance of progress-measure liftings.

It can replicate the behavior of existing attractor-based algorithms through controlled information discarding.

The approach unifies and interprets multiple quasi-polynomial algorithms within a common framework.

Abstract

Progress-measure lifting algorithms for solving parity games have the best worst-case asymptotic runtime, but are limited by their asymmetric nature, and known from the work of Czerwi\'nski et al. (2018) to be subject to a matching quasi-polynomial lower bound inherited from the combinatorics of universal trees. Parys (2019) has developed an ingenious quasi-polynomial McNaughton- Zielonka-style algorithm, and Lehtinen et al. (2019) have improved its worst-case runtime. Jurdzi\'nski and Morvan (2020) have recently brought forward a generic attractor-based algorithm, formalizing a second class of quasi-polynomial solutions to solving parity games, which have runtime quadratic in the size of universal trees. First, we adapt the framework of iterative lifting algorithms to computing attractor-based strategies. Second, we design a symmetric lifting algorithm in this setting, in which two lifting iterations, one for each player, accelerate each other in a recursive fashion. The symmetric algorithm performs at least as well as progress-measure liftings in the worst-case, whilst bypassing their inherent asymmetric limitation. Thirdly, we argue that the behaviour of the generic attractor-based algorithm of Jurdzinski and Morvan (2020) can be reproduced by a specific deceleration of our symmetric lifting algorithm, in which some of the information collected by the algorithm is repeatedly discarded. This yields a novel interpretation of McNaughton-Zielonka-style algorithms as progress-measure lifting iterations (with deliberate set-backs), further strengthening the ties between all known quasi-polynomial algorithms to date.