Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited

TL;DR

This paper revisits mean-payoff parity games to analyze nondeterministic strategies, providing complexity insights and a new algorithm, with implications for computing the most permissive winning strategies.

Contribution

It introduces a novel approach to measure permissiveness in parity games via mean-payoff parity games, proving complexity bounds and presenting a new solution algorithm.

Findings

Permissiveness measurement is in NP intersect coNP.

Opponent has a memoryless optimal strategy in mean-payoff parity games.

A new algorithm for solving mean-payoff parity games is proposed.

Abstract

We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number/weight of transitions blocked by the strategy. Using a translation into mean-payoff parity games, we prove that the problem of computing (the permissiveness of) a most permissive winning strategy is in NP intersected coNP. Along the way, we provide a new study of mean-payoff parity games. In particular, we prove that the opponent player has a memoryless optimal strategy and give a new algorithm for solving these games.