Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Half-Positional Objectives Recognized by Deterministic Büchi Automata

Patricia Bouyer, Antonio Casares, Mickael Randour, Pierre Vandenhove

TL;DR

This work addresses when ω-regular objectives recognized by deterministic Büchi automata admit memoryless optimal strategies for the protagonist across all arenas (half-positionality). It introduces a three-condition characterization tied to the right-congruence structure and the prefix-classifier, and proves sufficiency via a universal-graph framework while establishing necessity through automata-theoretic arguments. A polynomial-time algorithm is provided to decide half-positionality for DBA-recognizable objectives, with notable corollaries for prefix-independent cases (reducing to Büchi conditions) and finite-one-player-to-all-arena lifts. The results advance understanding of memory requirements in ω-regular games and offer a practical tool for automated synthesis and verification in systems specified by deterministic Büchi automata.

Abstract

In two-player games on graphs, the simplest possible strategies are those that can be implemented without any memory. These are called positional strategies. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a subclass of omega-regular objectives) that are half-positional, that is, for which the protagonist can always play optimally using positional strategies (both over finite and infinite graphs). Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.

Half-Positional Objectives Recognized by Deterministic Büchi Automata

TL;DR

This work addresses when ω-regular objectives recognized by deterministic Büchi automata admit memoryless optimal strategies for the protagonist across all arenas (half-positionality). It introduces a three-condition characterization tied to the right-congruence structure and the prefix-classifier, and proves sufficiency via a universal-graph framework while establishing necessity through automata-theoretic arguments. A polynomial-time algorithm is provided to decide half-positionality for DBA-recognizable objectives, with notable corollaries for prefix-independent cases (reducing to Büchi conditions) and finite-one-player-to-all-arena lifts. The results advance understanding of memory requirements in ω-regular games and offer a practical tool for automated synthesis and verification in systems specified by deterministic Büchi automata.

Abstract

In two-player games on graphs, the simplest possible strategies are those that can be implemented without any memory. These are called positional strategies. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a subclass of omega-regular objectives) that are half-positional, that is, for which the protagonist can always play optimally using positional strategies (both over finite and infinite graphs). Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
Paper Structure (45 sections, 33 theorems, 14 equations, 15 figures)

This paper contains 45 sections, 33 theorems, 14 equations, 15 figures.

Table of Contents

  1. Introduction
  2. Graph games and reactive synthesis.
  3. Half-positionality.
  4. $\omega$-regular objectives and deterministic Büchi automata.
  5. Universal graphs.
  6. Right congruence.
  7. Contributions.
  8. Technical overview.
  9. Other related works.
  10. Structure of the paper.
  11. Conference version.
  12. Preliminaries
  13. Games and positionality
  14. Graphs.
  15. Arenas and strategies.
  16. ...and 30 more sections

Key Result

Lemma 2.6

Let $w_1, w_2\in C^*$. If $w_1 \sim w_2$, then for all $w\in C^*$, $w_1w \sim w_2w$.

Figures (15)

  • Figure 1: A DBA (left) and its unique saturation (right). Transitions labeled with a $\bullet$ symbol are the Büchi transitions. In figures, automaton states are depicted with diamonds.
  • Figure 2: DBA $\mathcal{B}$ recognizing objective $W = (aa+bb)C^\omega$ (left), and an arena in which positional strategies do not suffice for $\mathcal{P}_{1}$ to play optimally for this objective (right). In figures, circles represent arena vertices controlled by $\mathcal{P}_{1}$.
  • Figure 3: A DBA recognizing the set of words containing $aa$ at some point (left), an arena in which positional strategies do not suffice for $\mathcal{P}_{1}$ to play optimally for this objective (right). Squiggly arrows indicate a sequence of edges or transitions (here, a sequence of two edges).
  • Figure 4: A DBA recognizing the set of words containing infinitely many occurrences of $a$, or containing $aa$ at some point.
  • Figure 5: DBA recognizing the objective $\mathsf{B\ddot{u}chi}(\{a\}) \cap \mathsf{B\ddot{u}chi}(\{b\})$ (left), and an arena in which positional strategies do not suffice for $\mathcal{P}_{1}$ to play optimally for this objective (right).
  • ...and 10 more figures

Theorems & Definitions (85)

  • Remark 2.1: $\varepsilon$-edges
  • Remark 2.2
  • Remark 2.3
  • Remark 2.4
  • Remark 2.5
  • Lemma 2.6
  • proof
  • Lemma 2.7
  • proof
  • Lemma 2.8
  • ...and 75 more