Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Playing Safe, Ten Years Later

Thomas Colcombet, Nathanaël Fijalkow, Florian Horn

TL;DR

The paper provides a general, topology-based characterization of the memory requirements for winning strategies in safety games on graphs: for any safety objective $W$, the minimal memory needed equals the width of the poset $(\mathrm{Res}(W),\subseteq)$ of non-empty left quotients. It develops upper and lower bounds, showing that $\text{mem}(W)$ lies between the width and the quotient size, with equalities in regular and well-founded finite-degree settings. The authors introduce a memory construction driven by left quotients and use a Dilworth-based decomposition to handle finite-degree cases, establishing half-positional results and exact memory counts in several concrete objective families. The framework yields exact memory requirements for generalized reachability (through the width of $\text{Res}(W)$) and demonstrates positional strategies in games with counters, with broad implications for synthesis and controller design in non-regular safety settings.

Abstract

We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety objectives. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety objective is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety objectives without any regularity assumptions. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.

Playing Safe, Ten Years Later

TL;DR

The paper provides a general, topology-based characterization of the memory requirements for winning strategies in safety games on graphs: for any safety objective , the minimal memory needed equals the width of the poset of non-empty left quotients. It develops upper and lower bounds, showing that lies between the width and the quotient size, with equalities in regular and well-founded finite-degree settings. The authors introduce a memory construction driven by left quotients and use a Dilworth-based decomposition to handle finite-degree cases, establishing half-positional results and exact memory counts in several concrete objective families. The framework yields exact memory requirements for generalized reachability (through the width of ) and demonstrates positional strategies in games with counters, with broad implications for synthesis and controller design in non-regular safety settings.

Abstract

We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety objectives. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety objective is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety objectives without any regularity assumptions. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.
Paper Structure (6 sections, 11 theorems, 10 equations, 6 figures)

This paper contains 6 sections, 11 theorems, 10 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Definitions
  3. Statements of the Results
  4. Proofs
  5. Examples and Applications
  6. Related Works

Key Result

Lemma 3.1

Let $\mathcal{G}$ be a game with a safety condition, and $v_0$ an initial vertex. If Eve has a winning strategy, then she has a positional winning strategy.

Figures (6)

  • Figure 1: Memory is necessary for safety objectives: to avoid seeing both $a$ and $b$, Eve must choose the same letter as Adam did in the first move, which requires two memory states.
  • Figure 2: The lower bound.
  • Figure 3: The outbidding objective: more $b$'s than $a$'s.
  • Figure 4: An outbidding game with infinite degree where Eve needs infinite memory to win.
  • Figure 5: The energy objective: always more $a$'s than $b$'s.
  • ...and 1 more figures

Theorems & Definitions (15)

  • Lemma 3.1: Folklore
  • Theorem 3.2
  • Corollary 3.3
  • Lemma 4.1
  • proof
  • Lemma 4.2: Upper bound in the regular case
  • proof
  • Lemma 4.3: Upper bound -- well founded assumption
  • Lemma 4.4: Upper bound -- finite degree assumption
  • proof
  • ...and 5 more