Strategy Derivation for Small Progress Measures

TL;DR

This paper introduces a new approach to Small Progress Measures for parity games that enables deriving winning strategies in a single pass, improving efficiency over previous methods.

Contribution

It provides a novel operational interpretation and modifies the algorithm to derive strategies in one pass, reducing the upper bound on strategy derivation.

Findings

Strategy derivation now in one pass

Reduced upper bound on strategy derivation time

Enhanced efficiency of parity game solving

Abstract

Small Progress Measures is one of the most efficient parity game solving algorithms. The original algorithm provides the full solution (winning regions and strategies) in $O(dm \cdot (n/\lceil d / 2 \rceil)^{\lceil d/2 \rceil})$ time, and requires a re-run of the algorithm on one of the winning regions. We provide a novel operational interpretation of progress measures, and modify the algorithm so that it derives the winning strategies for both players in one pass. This reduces the upper bound on strategy derivation for SPM to $O(dm \cdot (n/\lfloor d / 2 \rfloor)^{\lfloor d/2 \rfloor})$.