Source-linked AI summary
Generalized Mean-payoff and Energy Games
Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-Francois Raskin
TL;DR
Multiple-resource synthesis must account for quantitative objectives that may conflict, motivating generalized mean-payoff and energy games. The paper establishes finite-memory determinacy and inter-reducibility results, with coNP-complete finite-memory decision problems and NP-completeness for the memoryless winning-strategy question.
Problem
Resource-constrained reactive-system synthesis can involve multiple, potentially conflicting quantitative objectives, motivating generalized mean-payoff and energy games.
Source: §1 · p. 1Method
The paper studies strategy and computational complexity, establishing finite-memory determinacy and inter-reducibility for generalized mean-payoff and energy games.
Source: §1 · p. 2Results
Finite-memory decision problems are coNP-complete, while deciding whether Player 1 has a memoryless winning strategy is NP-complete.
Source: §1 · p. 2Takeaways & Limitations
Finite-memory strategies are relevant to reactive-system synthesis questions with ultimately periodic words.
Source: §1 · p. 2The complexity of generalized mean-payoff games with infinite-memory strategies remains open.
Source: §6 · p. 12
Abstract
from arXiv · showhide
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Generalized mean-payoff and energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of generalized energy games and show the inter-reducibility of generalized mean-payoff and energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.
1 Introduction
Multiple, potentially conflicting resource objectives motivate generalized mean-payoff and energy games as models for resource-constrained reactive-system synthesis. The section introduces their finite-memory strategy questions and reports determinacy, inter-reducibility, and complexity results.
Motivation
- The motivation is to model multiple, potentially conflicting quantitative objectives, such as minimizing response time and power consumption in resource-constrained systems.The paper studies multi-objective generalizations of mean-payoff and energy objectives.Source: §1 · p. 1
Game objectives
- Generalized mean-payoff games use integer-vector edge weights, and Player 1 wins when each coordinate’s mean value reaches its threshold.The section identifies finite-memory strategies as relevant to practical synthesis settings, including specifications interpreted over ultimately periodic words.Source: §1 · pp. 1–2
- In generalized energy games, Player 1 seeks an initial credit and a strategy that keep every coordinate’s running energy nonnegative against Player 2.Source: §1 · p. 2
Contributions
- Generalized energy and mean-payoff games are determined under finite-memory strategies, but not under memoryless strategies.For generalized energy games, finite-memory determinacy coincides with determinacy under arbitrary strategies; for generalized mean-payoff games, the two do not coincide.Source: §1 · p. 2
- Under finite-memory or memoryless strategies, generalized mean-payoff and generalized energy game problems are equivalent.The stated equivalence is restricted to the case where both players use strategies of the same specified kind.Source: §1 · p. 2
- Finite-memory decision problems are coNP-complete, improving the prior EXPSPACE upper bound; deciding whether Player 1 has a memoryless winning strategy is NP-complete.The coNP lower bound holds even for weights restricted to {−1, 0, 1}; memoryless NP-hardness holds with those weights or with arbitrary weights in dimension 2.Source: §1 · pp. 2–3
2 Generalized Mean-payoff and Energy Games
This section defines the multi-weighted game structures, objectives, strategies, and decision problems used in the paper. It also states determinacy for generalized mean-payoff and energy games and distinguishes unrestricted from finite-memory determinacy.
Game structures
- A multi-weighted game is a finite two-player graph whose edges carry integer vectors with dimension k; plays are infinite paths from the designated initial position.Source: §2 · p. 3
Strategies
- Strategies map finite play prefixes to moves; a finite-memory strategy is encoded by a finite-state Moore machine, and a memoryless strategy has one memory state.Source: §2 · pp. 3–4
Objectives
- The multi-energy objective requires every energy coordinate to stay nonnegative from an initial credit, while the multi-mean-payoff objective requires every coordinate’s mean payoff to meet its threshold.Source: §2 · p. 4
Decision problems
- The unknown initial credit problem asks whether some initial credit and Player 1 strategy win the multi-energy objective; the finite-memory mean-payoff threshold problem asks whether a finite-memory strategy meets a given threshold.The first problem permits arbitrary strategies, though the paper later shows finite memory suffices; the second explicitly restricts Player 1 to finite memory.Source: §2 · p. 4
Determinacy
- Generalized mean-payoff and energy games are determined, but finite-memory determinacy requires that a finite-memory player can win or spoil against finite-memory opponents.The text states that determinacy follows from the measurability of these objectives and a cited result.Source: §2 · pp. 4–5
3 Determinacy under Finite-memory and Inter-reducibility
The section proves finite-memory determinacy for generalized energy games and log-space inter-reducibility with finite-memory generalized mean-payoff games. It contrasts this with generalized mean-payoff games, where infinite memory may be necessary.
3 Determinacy under Finite-memory and Inter-reducibility
- In generalized energy games, Player 1 needs only finite memory to win, while Player 2 can spoil with memoryless play, yielding finite-memory determinacy.For these games, finite-memory determinacy coincides with determinacy under arbitrary strategies.Source: §3 · pp. 5–6
- A winning energy strategy can be converted to finite memory by truncating its unfolding when a later node revisits a state with at least as much energy.The construction reuses the subtree of the earlier node because the later energy level is no lower.Source: §3 · p. 5
- The unknown-initial-credit energy problem is equivalent to the finite-memory mean-payoff threshold problem at threshold {0}^k, and the problems are log-space inter-reducible.Source: §3 · pp. 5–7
- Generalized mean-payoff games are determined under finite memory, but this does not coincide with arbitrary-strategy determinacy; infinite memory may be necessary to win.Source: §3 · pp. 7–8
4 coNP-completeness for Finite-Memory Strategies
This section establishes coNP-completeness for the unknown-initial-credit and mean-payoff threshold problems, using a polynomial verification argument and a reduction from complement 3SAT.
4 coNP-completeness for Finite-Memory Strategies
- The unknown-initial-credit and mean-payoff threshold problems for multi-weighted two-player games are coNP-complete.The lower bound holds even when weights are restricted to {−1, 0, 1}.Source: §4 · pp. 8, 10
- For the coNP upper bound, guess a memoryless Player 2 strategy and check in polynomial time whether it is winning.After fixing that strategy, the resulting one-player graph is checked for a reachable circuit with nonnegative effect in every dimension; polynomial-time zero-circuit detection supports this check.Source: §4 · pp. 8–9
- A reduction from the complement of 3SAT establishes coNP-hardness for the unknown-initial-credit problem.The construction uses one weight component per literal and restricts weights to {−1, 0, 1}.Source: §4 · pp. 9–10
- When the 3SAT formula is satisfiable, Player 2 can choose true literals so that a literal recurring infinitely often causes its complementary component to decrease without bound.This makes Player 2 winning for every finite initial credit.Source: §4 · p. 9
5 NP-completeness for Memoryless Strategies
For memoryless Player 1 strategies, the unknown-initial-credit and mean-payoff threshold problems are NP-complete, with membership and hardness established through polynomial verification and reductions.
5 NP-completeness for Memoryless Strategies
- A memoryless Player 1 strategy is a polynomial witness, and the resulting game can be checked in polynomial time for both problems.Verification checks for negative cycles in every dimension for energy, or threshold-violating cycles for mean-payoff.Source: §5 · p. 10
- The problems are NP-hard even for one-player games with dimension k = 2 and arbitrary integral weights.This hardness follows by reducing Knapsack, representing item selection with two weight coordinates for profit and item weight.Source: §5 · p. 11
- NP-hardness also holds for one-player games with weights restricted to {−1, 0, 1}, when the dimension is arbitrary.The supplied result contrasts this with polynomial-time solvability for two dimensions under the same weight restriction.Source: §5 · p. 11
- A reduction from 3SAT establishes NP-hardness by encoding each variable’s truth choice and checking that every clause is satisfied.A satisfying assignment yields a winning memoryless strategy, and such a strategy yields a satisfying assignment.Source: §5 · pp. 11–12
- The unknown-initial-credit and mean-payoff threshold problems are NP-complete when Player 1 is restricted to memoryless strategies.The classification also holds for one-player game structures.Source: §5 · pp. 11–12
6 Conclusion
The paper establishes finite-memory determinacy and inter-reducibility for generalized mean-payoff and energy games, improving finite-memory complexity bounds to coNP-complete. It leaves infinite-memory mean-payoff complexity and exact or approximate Pareto-curve computation open.
6 Conclusion
- The paper establishes finite-memory determinacy and inter-reducibility for generalized mean-payoff and energy games, improving complexity bounds from EXPSPACE to coNP-complete.The stated complexity result concerns finite-memory strategies.Source: §6 · p. 12
- The complexity of generalized mean-payoff games with infinite-memory strategies and computation of the exact or approximate Pareto curve remain open.Infinite-memory winning strategies are more powerful than finite-memory strategies for generalized mean-payoff games.Source: §6 · p. 12