Source-linked AI summary
Energy Parity Games
Krishnendu Chatterjee, Laurent Doyen
TL;DR
Energy parity games ask how to satisfy an infinite-run parity condition while keeping accumulated energy positive in resource-constrained settings. The paper analyzes strategy memory and decision complexity, gives an algorithm, and connects the model to mean-payoff parity games. It shows that winning strategies may need exponential memory, yet winner determination is in NP ∩coNP, with polynomial equivalence to mean-payoff parity games.
Problem
Resource-constrained reactive systems need specifications combining qualitative functional requirements with quantitative resource limits.
Method
The paper studies weighted turn-based parity games, characterizes winning-strategy structure, and develops algorithms reducing energy parity games to reachability and energy games.
Results
Winning strategies require at most n · d · W memory and may require exponential memory, while winner determination lies in NP ∩coNP and is polynomially equivalent to mean-payoff parity games.
Takeaways & Limitations
Energy parity games admit finite-memory winning strategies and memoryless spoiling strategies, providing a tractable complexity characterization and a simpler route to mean-payoff parity games.
Takeaways & Limitations
For some proofs, rational weights are allowed, although complexity results assume integer weights encoded in binary.
Abstract
from arXiv · showhide
Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (i.e., the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objective. Our main results are as follows: (a) exponential memory is necessary and sufficient for winning strategies in energy parity games; (b) the problem of deciding the winner in energy parity games can be solved in NP \cap coNP; and (c) we give an algorithm to solve energy parity by reduction to energy games. We also show that the problem of deciding the winner in energy parity games is polynomially equivalent to the problem of deciding the winner in mean-payoff parity games, while optimal strategies may require infinite memory in mean-payoff parity games. As a consequence we obtain a conceptually simple algorithm to solve mean-payoff parity games.
1 Introduction
Energy parity games combine qualitative parity requirements with quantitative energy constraints for resource-constrained reactive systems. The paper establishes bounds on strategy memory, decision complexity, algorithms, and connections to mean-payoff parity games.
- Motivation: Resource-constrained reactive systems require specifications that jointly express quantitative resource limits and qualitative functional requirements.The paper places energy parity games in the context of synthesis for systems such as embedded devices.
- Problem setting: Energy parity games combine a parity condition with the requirement that accumulated edge weights remain positive.They model infinite two-player games on weighted graphs with priorities on states and binary-encoded integer weights.
- Main results: n · d · W memory is sufficient for winning strategies, while exponential memory may already be necessary in one-player games.Here n is the state-space size, d the number of priorities, and W the maximum absolute edge weight.
- Main results: The winner-decision problem for energy parity games lies in NP ∩coNP despite potentially exponential memory for winning strategies.The NP argument uses special structures that decompose such strategies into two memoryless strategies, while memoryless spoiling strategies provide the coNP upper bound.
- Algorithms: The paper presents an algorithm reducing energy parity solving to iterative reachability and energy games, with complexity exponential in states and linear in the largest weight.This gives an algorithmic route to computing winning outcomes and minimum initial credit.
- Connections: Energy parity and mean-payoff parity games are polynomially equivalent, yielding an NP ∩coNP result and a conceptually simpler mean-payoff algorithm.The comparison also highlights that optimal mean-payoff parity strategies may require infinite memory.
2 Definitions
The paper formalizes turn-based games, strategies, weights, and combined parity-energy objectives. It defines winning and initial-credit questions while relating the model to standard parity and energy games.
- Game model: A game graph partitions finite states between two players, with the owner of the current state choosing each outgoing successor.Player-1 games are the special case in which every state belongs to player 1.
- Strategies: Strategies map finite histories to legal successor states, while finite-memory strategies use a finite transducer with update and next-move functions.The strategy size is the number of memory values in the transducer.
- Weights and energy: The energy level of a finite play prefix is the sum of its edge weights, with positive weights representing rewards and negative weights representing costs.Weights are integer and binary encoded for complexity results, and W denotes the largest absolute edge weight.
- Objectives: The parity objective requires the least priority occurring infinitely often to be even.Parity objectives are prefix-independent, so finite prefixes do not affect satisfaction.
- Objectives: The energy objective requires the accumulated energy, starting from initial credit c0, to remain nonnegative throughout the play.Mean-payoff and combined parity-energy objectives are defined alongside it.
- Winning and credit: The finite initial credit problem asks whether some finite c0 and winning strategy exist from a given state, while minimum initial credit is the least such value.A strategy is optimal when it wins using the minimum initial credit.
3 Strategy Complexity of Energy Parity Games
Energy parity games require finite memory for player 1, with an exponential bound that is sometimes necessary, while player 2 needs only memoryless strategies. The paper establishes these bounds through constructions combining energy management with parity-preserving strategies.
- Strategy memory: n · d · W memory suffices for player 1’s winning strategies, where n is the number of states, d the priorities, and W the maximum absolute edge weight.Because weights are binary encoded, this bound is exponential in the input representation.
- Opponent strategies: Memoryless winning strategies exist for player 2 in all energy parity games.This result supports the coNP upper bound for the decision problem.
- Construction: The winning-strategy construction alternates good-for-energy strategies with attractor strategies while preserving the parity condition across phases.Its memory analysis combines energy-level tracking with recursively solved subgames, yielding the n · d · W bound.
4 Computational Complexity of Energy Parity Games
The initial-credit problem for energy parity games is in NP ∩coNP. The NP proof uses structured winning strategies, while the coNP proof relies on memoryless spoiling strategies and polynomial verification for the resulting player-1 games.
- Verification: Good-for-energy strategies can be checked in polynomial time using shortest-path procedures on reachable cycles.The checks require nonnegative cycle sums generally and strictly positive sums for relevant odd-priority subgraphs.
- Inductive proof: The two-priority base cases use memoryless strategies for energy coBüchi games and complementary good-for-energy and Büchi strategies.These cases provide the foundation for the inductive NP argument for arbitrary parity objectives.
- NP membership: The NP upper bound guesses the winning-state set and structured strategies, then verifies their energy and parity properties.For the general case, the construction proceeds inductively over the number of priorities.
- Main complexity result: The problem of deciding whether a finite initial credit exists for energy parity games is in NP ∩coNP.The NP and coNP bounds are obtained separately from structured winning certificates and memoryless spoiling strategies.
- coNP membership: The coNP upper bound follows because player 2 has memoryless spoiling strategies and the resulting player-1 energy parity problem is polynomial-time decidable.The polynomial-time player-1 procedure checks the initial-credit problem directly.
5 Algorithm for Energy Parity Games
The algorithm decides energy parity games by transforming cycle weights to encode parity and recursively combining energy-game solutions with attractor and fixpoint computations.
- Weight modification: It constructs modified weights so zero-sum simple cycles become positive when their least priority is even and negative when it is odd.Winning the resulting energy game is equivalent to having a memoryless good-for-energy strategy in the original game.
- Complexity: The algorithm has complexity exponential in the number of states and linear in the largest weight.Attractors are computed during recursive calls, whose number is bounded by |Q| while priorities decrease across calls.
- Weight modification: Computing a memoryless good-for-energy strategy takes O(|E| · |Q|^d+1 · W) time.The modified maximum weight is W′ = W · |Q|^d.
- Recursive solution: A recursive fixpoint algorithm generalizes the classical McNaughton–Zielonka parity-game algorithm.It repeatedly computes good-for-energy states, decomposes them by priority, applies attractors, and recurses on reduced subgraphs.
- Complexity: The algorithm runs in O(|E| · d · |Q|^d+2 · W) time for the finite initial credit problem.Here d is the number of priorities and W is the largest weight.
- Special cases: For energy Büchi games, the time complexity specializes to O(|E| · |Q|^4 · W).This follows because the number of priorities is constant, d = 2.
6 Relationship with Mean-payoff Parity Games
The paper establishes a tight relationship between energy parity and mean-payoff parity games through a weight shift, transferring winner-decision results and algorithms between them. This yields NP ∩coNP membership and a conceptually simpler solution method for mean-payoff parity games.
- Equivalence: Energy parity games and mean-payoff parity games are polynomially equivalent.The paper describes this relationship as tight and uses it to transfer decision and algorithmic results.
- Equivalence: Adding ε = 1/(|Q|+1) to every weight preserves whether Player 1 has a winning strategy.Player 1 wins the mean-payoff parity game iff Player 1 wins the corresponding energy parity game with shifted weights.
- Proof strategy: The reduction uses finite-memory strategies and an initial credit sufficient to offset the finite strategy graph's accumulated deficit.The proof considers the strategy-induced graph and assigns initial credit |Gσ| · W in one direction.
- Consequences: Winner determination for mean-payoff parity games belongs to NP ∩coNP.This is stated as Corollary 1 of the equivalence result.
- Consequences: Mean-payoff parity games can be solved in O(|E| · d · |Q|^d+2 · W · (|Q| + 1)) time.The resulting algorithm is described as conceptually simpler while having essentially the same complexity as the prior approach.