The Power of Counting Steps in Quantitative Games

TL;DR

The paper investigates the memory requirements for winning strategies in deterministic infinite-duration graph games with quantitative objectives. It derives upper and lower bounds for strategy complexity in mean-payoff and total-payoff objectives, focusing on step-counter strategies (with possible one-bit memory) across finitely and infinitely branching arenas. It proves that certain prefix-independent Pi2 objectives such as $\overline{\mathsf{MP}}_{\ge 0}$ and $\overline{\mathsf{TP}}_{= +\infty}$ admit step-counter strategies uniformly, while a non-prefix-independent Pi2 objective $\overline{\mathsf{TP}}_{\ge 0}$ requires step-counter plus one bit, not just step counter. Together these results place many classical quantitative objectives at the second level of the Borel hierarchy in relevant settings and clarify when simple infinite-memory structures suffice for reactive synthesis.

Abstract

We study deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs. We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of limsup mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain liminf total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy.

Figures (8)

• Figure 1: Arenas implementing the "match the number" game. Circles designate vertices controlled by Player 1 and squares designate Player 2. The edge labels indicate that for every $i\in\mathbb{N}$ there is a distinct edge with weight $-i$ from $s$ to $t$, and $+i$ from $t$ to $q$ or from $t$ to $s$. For $\mathcal{A}_1$, consider the objective "sum of weights exceeds $0$". Player 1 can always match and thus win, but needs unbounded memory. The arena $\mathcal{A}'_1$ shows a repeated version for the $\limsup$mean-payoff objective.
• Figure 2: The arena $\mathcal{A}_2$ is acyclic and every vertex has finite in- and out-degree. We recall that circles are controlled by Player 1 and squares by Player 2.
• Figure 3: The arena $\mathcal{A}_3$. Arrows are shorthand for paths of length $2i+1$ with edge weights $-1$, and are shorthand for paths of length $3$ with edge weights $0$.
• Figure 4: The arena $\mathcal{A}_4$. Arrows are shorthand for paths of length $2i+3$ with total payoff $-2(i+1)$. From a vertex $t_i$, Player 1 either exits to $r_0$ or moves to the gadget in \ref{['fig:LB-3-delay']}.
• Figure 5: The delay gadget from vertex $t_i$ in arena $\mathcal{A}_4$. The arrows from $t_i^j$ to $t_{i+j}$ are shorthand for paths of length $2j$ and payoff $-2j+1$.

Theorems & Definitions (35)

• Lemma 1
• Remark 2
• Lemma 2
• Lemma 3
• Lemma 4
• Definition 5
• Lemma 5
• Lemma 6
• Lemma 7
• Theorem 8