Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fair Quantitative Games

Ashwani Anand, Satya Prakash Nayak, Ritam Raha, Irmak Sağlam, Anne-Kathrin Schmuck

TL;DR

This paper advances the study of quantitative two-player games by introducing and analyzing fair energy and fair mean-payoff games under strong-transition fairness. It develops gadget-based reductions that transform fair games into standard mean-payoff or energy games on expanded arenas, enabling pseudo-polynomial algorithms and precise determinacy and memory results. In particular, 1-fair mean-payoff games admit a linearly enlarged reduction with concrete complexity bounds, while 2-fair variants exhibit different determinacy properties, with some cases not being determined. Overall, the work demonstrates that strong-transition fairness integrates well with quantitative objectives and extends gadget-techniques beyond the omega-regular domain, offering practical solution methods for reactive synthesis in CPS contexts.

Abstract

We examine two-player games over finite weighted graphs with quantitative (mean-payoff or energy) objective, where one of the players additionally needs to satisfy a fairness objective. The specific fairness we consider is called 'strong transition fairness', given by a subset of edges of one of the players, which asks the player to take fair edges infinitely often if their source nodes are visited infinitely often. We show that when fairness is imposed on player 1, these games fall within the class of previously studied omega-regular mean-payoff and energy games. On the other hand, when the fairness is on player 2, to the best of our knowledge, these games have not been previously studied. We provide gadget-based algorithms for fair mean-payoff games where fairness is imposed on either player, and for fair energy games where the fairness is imposed on player 1. For all variants of fair mean-payoff and fair energy (under unknown initial credit) games, we give pseudo-polynomial algorithms to compute the winning regions of both players. Additionally, we analyze the strategy complexities required for these games. Our work is the first to extend the study of strong transition fairness, as well as gadget-based approaches, to the quantitative setting. We thereby demonstrate that the simplicity of strong transition fairness, as well as the applicability of gadget-based techniques, can be leveraged beyond the omega-regular domain.

Fair Quantitative Games

TL;DR

This paper advances the study of quantitative two-player games by introducing and analyzing fair energy and fair mean-payoff games under strong-transition fairness. It develops gadget-based reductions that transform fair games into standard mean-payoff or energy games on expanded arenas, enabling pseudo-polynomial algorithms and precise determinacy and memory results. In particular, 1-fair mean-payoff games admit a linearly enlarged reduction with concrete complexity bounds, while 2-fair variants exhibit different determinacy properties, with some cases not being determined. Overall, the work demonstrates that strong-transition fairness integrates well with quantitative objectives and extends gadget-techniques beyond the omega-regular domain, offering practical solution methods for reactive synthesis in CPS contexts.

Abstract

We examine two-player games over finite weighted graphs with quantitative (mean-payoff or energy) objective, where one of the players additionally needs to satisfy a fairness objective. The specific fairness we consider is called 'strong transition fairness', given by a subset of edges of one of the players, which asks the player to take fair edges infinitely often if their source nodes are visited infinitely often. We show that when fairness is imposed on player 1, these games fall within the class of previously studied omega-regular mean-payoff and energy games. On the other hand, when the fairness is on player 2, to the best of our knowledge, these games have not been previously studied. We provide gadget-based algorithms for fair mean-payoff games where fairness is imposed on either player, and for fair energy games where the fairness is imposed on player 1. For all variants of fair mean-payoff and fair energy (under unknown initial credit) games, we give pseudo-polynomial algorithms to compute the winning regions of both players. Additionally, we analyze the strategy complexities required for these games. Our work is the first to extend the study of strong transition fairness, as well as gadget-based approaches, to the quantitative setting. We thereby demonstrate that the simplicity of strong transition fairness, as well as the applicability of gadget-based techniques, can be leveraged beyond the omega-regular domain.

Paper Structure

This paper contains 9 sections, 2 theorems, 3 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Contributions
  4. Preliminaries
  5. Weighted Game Arena
  6. Fair Game Arena
  7. Example: Mean-Payoff vs Fair Mean-Payoff Games
  8. Solving Fair Mean-Payoff Games
  9. Proof of \ref{['thm:mpgadgetcorrectness']} for 1-fair Mean-Payoff Games

Key Result

theorem thmcountertheorem

Let $(G, E_f, \mathtt{MP}^f_0)$ be a fair mean-payoff game with threshold $0$, where $G = (Q, E, w)$, $w : E \to [-W, W]$, and $|Q|=n$. Then there exists a mean-payoff game $G'= (Q',E',w')$ where $Q' \supseteq Q$, $|Q'|\leq 6n$ and $w' : E' \to [-W', W']$ with $W' = n^2W + n$ such that $\mathtt{Win}

Figures (2)

  • Figure 1:
  • Figure 2: Gadgets for converting fair mean-payoff games to mean-payoff games. Edges are labeled with their weights. The edges labeled with $w$ represent: an edge from a gadget node to a node $q' \in E(q)$ or $E_f(q)$ carry the weight $w(q, q')$.

Theorems & Definitions (3)

  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • remark thmcounterremark