Smaller Progress Measures and Separating Automata for Parity Games

TL;DR

This paper introduces optimized separating automata for parity games, achieving the smallest known state spaces by refining previous progress measure techniques, thus advancing the efficiency of solving such games.

Contribution

It proposes new adjustments to existing automata-based methods, resulting in the most succinct progress measures for parity games to date.

Findings

Achieved a statespace size matching Jurdzinski and Lasic's methods.

Further reduced the statespace beyond previous approaches.

Enhanced the efficiency of solving parity games with smaller automata.

Abstract

Calude et al. have recently shown that parity games can be solved in quasi-polynomial time, a landmark result that has led to a number of approaches with quasi-polynomial complexity. Jurdinski and Lasic have further improved the precise complexity of parity games, especially when the number of priorities is low (logarithmic in the number of positions). Both of these algorithms belong to a class of game solving techniques now often called separating automata: deterministic automata that can be used as witness automata to decide the winner in parity games up to a given number of states and colours. We suggest a number of adjustments to the approach of Calude et al. that lead to smaller statespaces. These include and improve over those earlier introduced by Fearnley et al. We identify two of them that, together, lead to a statespace of exactly the same size Jurdzinski and Lasic's concise progress measures, which currently hold the crown as smallest statespace. The remaining improvements, hence, lead to a further reduction in the size of the statespace, making our approach the most succinct progress measures available for parity games.