Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The memory of $ω$-regular and BC($Σ_2^0$) objectives

Antonio Casares, Pierre Ohlmann

TL;DR

This work advances the theory of strategy memory for infinite-duration games by extending memory analysis to BCΣ objectives through a unifying framework of $k$-wise $\varepsilon$-complete automata and universal graphs. It proves a finite-to-infinite lift for ω-regular objectives, placing the memory decision in NP, and establishes a product bound for memory under unions when one operand is prefix-independent. The authors introduce a constructive toolbox—$k$-blowups, $\varepsilon$-completions, cascade products, and universal graphs—enabling both existence proofs and practical automata constructions, with a detailed finitary and infinitary treatment. They also extend the union principle to BCΣ objects via an $\varepsilon$-completion of a product with a parity-universal automaton, yielding a tight memory bound $k_1k_2$ under suitable conditions. Overall, the paper significantly broadens memory theory from ω-regular to BCΣ objectives and provides NP-decidability results, universal-graph characterisations, and robust union bounds that generalize Kopczyński’s conjecture in this broader setting.

Abstract

In the context of 2-player zero-sum infinite-duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with <= k states of memory. For omega-regular objectives, checking whether the memory equals a given number k was not known to be decidable. In this work, we focus on objectives in BC(Sigma0^2), i.e. recognised by a potentially infinite deterministic parity automaton. We provide a class of automata that recognise objectives with memory <= k, leading to the following results: (1) For omega-regular objectives, the memory over finite and infinite games coincides and can be computed in NP. (2) Given two objectives W1 and W2 in BC(Sigma0^2) and assuming W1 is prefix-independent, the memory of W1 U W2 is at most the product of the memories of W1 and W2. Our results also apply to chromatic memory, the variant where strategies can update their memory state only depending on which colour is seen.

The memory of $ω$-regular and BC($Σ_2^0$) objectives

TL;DR

This work advances the theory of strategy memory for infinite-duration games by extending memory analysis to BCΣ objectives through a unifying framework of -wise -complete automata and universal graphs. It proves a finite-to-infinite lift for ω-regular objectives, placing the memory decision in NP, and establishes a product bound for memory under unions when one operand is prefix-independent. The authors introduce a constructive toolbox—-blowups, -completions, cascade products, and universal graphs—enabling both existence proofs and practical automata constructions, with a detailed finitary and infinitary treatment. They also extend the union principle to BCΣ objects via an -completion of a product with a parity-universal automaton, yielding a tight memory bound under suitable conditions. Overall, the paper significantly broadens memory theory from ω-regular to BCΣ objectives and provides NP-decidability results, universal-graph characterisations, and robust union bounds that generalize Kopczyński’s conjecture in this broader setting.

Abstract

In the context of 2-player zero-sum infinite-duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with <= k states of memory. For omega-regular objectives, checking whether the memory equals a given number k was not known to be decidable. In this work, we focus on objectives in BC(Sigma0^2), i.e. recognised by a potentially infinite deterministic parity automaton. We provide a class of automata that recognise objectives with memory <= k, leading to the following results: (1) For omega-regular objectives, the memory over finite and infinite games coincides and can be computed in NP. (2) Given two objectives W1 and W2 in BC(Sigma0^2) and assuming W1 is prefix-independent, the memory of W1 U W2 is at most the product of the memories of W1 and W2. Our results also apply to chromatic memory, the variant where strategies can update their memory state only depending on which colour is seen.

Paper Structure

This paper contains 28 sections, 31 theorems, 28 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Finite-to-infinite lift.
  3. Unions of objectives.
  4. Our toolbox: Universal graphs and $\varepsilon$-completable automata.
  5. Preliminaries
  6. Graphs, games and memory
  7. Memory.
  8. Automata
  9. Cascade products.
  10. $\varepsilon$-completability and universal graphs
  11. Characterisation of objectives in $\BCSigma$ with memory $\leq k$
  12. Existence of $k$-wise $\varepsilon$-complete automata: infinitary proof
  13. Proof overview
  14. A combinatorial lemma: Extracting homogeneous subtrees
  15. Definition of $\mathcal{B}$
  16. ...and 13 more sections

Key Result

Lemma 2

Let $\mathcal{A}$ be an automaton with index $d$ and $S$ be a "$d$-graph" satisfying $\Parity_d$. Then $\mathcal{A} \casc S$ is "well-founded" and "satisfies" $L(\mathcal{A})$.

Figures (1)

  • Figure 1: A 2-automaton recognising $W=\mathtt{No}(b) \vee \mathtt{Fin}(aa) \vee {\mathtt{Inf}}(cc)$, where $p$ is assumed to have a different "memory state" than $q_0,q_1$ and $q_2$. It is "$2$-wise $\varepsilon$-completable" by adding the indicated "$\varepsilon$-transitions". A "completion" also contains the transitions $q_2\xrightarrow{\varepsilon:0,1,2} q_0$, as well as all transitions $q_i \xrightarrow{\varepsilon:3} q_{j}$ for $i>j$, and transitions $p \xrightarrow{\varepsilon:y} p$ for $y$ odd; these are omitted for ease of reading. However, it is not "chromatic@@aut" since reading $c$ may or may not switch the "memory state".

Theorems & Definitions (41)

  • Conjecture 1: ""Generalised Kopczyński's conjecture""
  • Lemma 2
  • Example 3
  • Theorem 4: Adapted from Lemma 3.4 in CO25LMCS
  • Theorem 5: Theorem 3.1 in CO25LMCS
  • Lemma 6: CO24Arxiv
  • Theorem 7: Main characterisation
  • Corollary 8: Finite-to-infinite lift
  • Corollary 9: Decidability in $\textbf{NP}$
  • Theorem 10: Union has bounded memory
  • ...and 31 more