Priority Promotion with Parysian Flair

TL;DR

This paper introduces a hybrid algorithm that combines priority promotion with Parys' quasi-polynomial approach to efficiently solve large parity games, blending practical effectiveness with theoretical guarantees.

Contribution

It presents a novel interface that unites priority promotion and Parys' algorithm, overcoming previous incompatibilities and achieving both efficiency and quasi-polynomial guarantees.

Findings

The hybrid algorithm is effective in practice.

It maintains quasi-polynomial time guarantees.

The approach outperforms existing methods in large parity games.

Abstract

We develop an algorithm that combines the advantages of priority promotion - one of the leading approaches to solving large parity games in practice - with the quasi-polynomial time guarantees offered by Parys' algorithm. Hybridising these algorithms sounds both natural and difficult, as they both generalise the classic recursive algorithm in different ways that appear to be irreconcilable: while the promotion transcends the call structure, the guarantees change on each level. We show that an interface that respects both is not only effective, but also efficient.