Characterising memory in infinite games

TL;DR

This work extends Ohlmann's universal-graph framework from purely positional objectives to objectives with finite or infinite memory bounds in infinite-duration turn-based games on graphs. By introducing ε-separated monotone universal graphs and related constructs, the authors establish a correspondence: an objective has ε-memory ≤ μ exactly when suitable universal structures exist with breadth bound μ (and similarly for ε-chromatic memory). They also develop a structuration lemma linking finite-memory structure with universal graphs, prove auxiliary results for prefix-increasing/prefix-independent objectives, and illustrate the framework through concrete examples (including Muller and topologically closed objectives). The paper further explores closure properties under lexicographic products, unions, and intersections, and highlights limitations via counterexamples. These results provide a general, graph-theoretic tool to derive memory upper bounds and to reason about the compositional behavior of memory-assisted objectives in infinite games.

Abstract

This paper is concerned with games of infinite duration played over potentially infinite graphs. Recently, Ohlmann (LICS 2022) presented a characterisation of objectives admitting optimal positional strategies, by means of universal graphs: an objective is positional if and only if it admits well-ordered monotone universal graphs. We extend Ohlmann's characterisation to encompass (finite or infinite) memory upper bounds. We prove that objectives admitting optimal strategies with $\varepsilon$-memory less than $m$ (a memory that cannot be updated when reading an $\varepsilon$-edge) are exactly those which admit well-founded monotone universal graphs whose antichains have size bounded by $m$. We also give a characterisation of chromatic memory by means of appropriate universal structures. Our results apply to finite as well as infinite memory bounds (for instance, to objectives with finite but unbounded memory, or with countable memory strategies). We illustrate the applicability of our framework by carrying out a few case studies, we provide examples witnessing limitations of our approach, and we discuss general closure properties which follow from our results.

Figures (19)

• Figure 1: On the left, a "game" with "objective" $W = (ab)^\omega$; in words, "Eve" should ensure that the play alternates between $a$-edges and $b$-edges. We represent Eve's vertices as circles and Adam's as squares. On the right, a winning "strategy" for "Eve" which uses one state of memory for $v_0$, one state of memory for $v_1$, and two states of memory for $v_2$. Note that two "states of memory" for $v_2$ are required here: a "positional" "strategy" would always follow the same self-loop and therefore cannot "win". One can prove that any "game" with "objective" $W$ which is won by "Eve" can be won even when restricting to "strategies" with two "states of memory", such as the one above. To conclude, the memory requirements for $W$ is exactly two.
• Figure 2: A summary of our main contributions. The three larger boxes correspond to the three regimes encompassed by our results: finite memory, locally finite memory and larger "cardinal" bounds. Each of the smaller boxes correspond to classes of "objectives", where "struct." stands for "existence of "well-founded" "monotone" "universal" graphs"; for example, the box labelled "$\varepsilon$-separated struct. breadth $\leq m$" stands for "existence of "$\varepsilon$-separated" "well-founded" "monotone" "universal" graphs of "breadth" $\leq m$". The dotted implications follow from combining other implications in the figure. For $m=1$, all notions collapse to a single equivalence, which corresponds to Ohlmann's characterisation.
• Figure 3: Diagram illustrating the definition of a strategy. We use squares to represent vertices controlled by Adam and circles for vertices controlled by Eve. In this figure, it does not matter who controls $v'$.
• Figure 4: An "$\varepsilon$-separated" "chromatic@@epsGraph" "monotone" graph of "breadth" 2. Note that $\xrightarrow{\varepsilon}$ defines a total order on each $V_i$ (edges following from transitivity are not represented). Many edges which follow from "monotonicity" are not depicted, the dotted edges give a few examples.
• Figure 5: An illustration for the construction of the bounded-memory strategy $\mathcal{S}$ in the proof of Theorem \ref{['thm:implication_non_eps']}.

Theorems & Definitions (67)

• Lemma 2.1
• proof
• Proposition 2.2
• proof : Proof of Proposition \ref{['prop:non-strict-ineq-for-eps-memory']}
• Remark 2.3
• Remark 2.4
• Theorem 3.1
• Theorem 3.2
• Remark 3.3
• proof : Proof of Theorem \ref{['thm:implication_non_eps']}