2014/10/17 by Yaron Velner, Velner, Yaron
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Machine Learning (cs.LG)
paper · pdf · doi:10.48550/arxiv.1410.5703
openalex publication_date 2014/10/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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(x1) ≤ 0 \vee \LimAvg(x2)≥ 0 \wedge \LimAvg(x3) ≥ 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.