Robust Multidimensional Mean-Payoff Games are Undecidable

TL;DR

This paper proves that determining the winner in robust multidimensional mean-payoff games with arbitrary strategies is undecidable, extending previous results that linked finite-memory strategies to an open problem.

Contribution

It establishes the undecidability of multidimensional mean-payoff games when both players can use infinite-memory strategies, a significant extension of prior work on finite-memory strategies.

Findings

Undecidability of the problem with infinite-memory strategies

Extension of previous finite-memory results to infinite-memory context

Connection to Hilbert's Tenth problem over rationals

Abstract

Mean-payoff games play a central role in quantitative synthesis and verification. In a single-dimensional game a weight is assigned to every transition and the objective of the protagonist is to assure a non-negative limit-average weight. In the multidimensional setting, a weight vector is assigned to every transition and the objective of the protagonist is to satisfy a boolean condition over the limit-average weight of each dimension, e.g., $\LimAvg(x_1) \leq 0 \vee \LimAvg(x_2)\geq 0 \wedge \LimAvg(x_3) \geq 0$. We recently proved that when one of the players is restricted to finite-memory strategies then the decidability of determining the winner is inter-reducible with Hilbert's Tenth problem over rationals (a fundamental long-standing open problem). In this work we allow arbitrary (infinite-memory) strategies for both players and we show that the problem is undecidable.