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

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.

30 pages, revised version

References in corpus (1)

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

Cited by in corpus (10)

• Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited
• Permissive Controller Synthesis for Probabilistic Systems
• SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes
• Synthesizing Permissive Winning Strategy Templates for Parity Games
• A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
• Down the Borel Hierarchy: Solving Muller Games via Safety Games
• Strategy Synthesis for Multi-dimensional Quantitative Objectives
• Quantitative Reductions and Vertex-Ranked Infinite Games (Full Version)
• Quantitative Reductions and Vertex-Ranked Infinite Games
• Synthesis from LTL Specifications with Mean-Payoff Objectives