Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Automata-Based Approach to Games with $ω$-Automatic Preferences

Véronique Bruyère, Emmanuel Filiot, Christophe Grandmont, Jean-François Raskin

TL;DR

This paper generalizes game-theoretic analysis on graphs to $ω$-automatic preferences, where each player's objective is specified by a $ω$-automatic relation accepted by a deterministic parity automaton. The authors define a generalized value as the set of plays a player can guarantee to improve upon and show this set is $ω$-regular, recognizable by a polynomial-size alternating parity automaton, enabling automata-based solutions for threshold problems, Nash equilibria, and rational synthesis. They obtain tight complexity results: the threshold problem and NE existence are $PSPACE$-complete; cooperative rational synthesis is $PSPACE$-complete while non-cooperative rational synthesis is undecidable; Pareto-optimal NE outcomes exist with $EXPSPACE$ membership and $PSPACE$-hardness. The results provide a unified automata-theoretic framework for reasoning about arbitrary $ω$-automatic preferences and have implications for verification and synthesis of reactive systems. The paper also outlines future directions, including robust equilibrium refinements (e.g., subgame-perfect equilibria) and extensions beyond $ω$-automatic to broader rational relations.

Abstract

This paper studies multiplayer turn-based games on graphs in which player preferences are modeled as $ω$-automatic relations given by deterministic parity automata. This contrasts with most existing work, which focuses on specific reward functions. We conduct a computational analysis of these games, starting with the threshold problem in the antagonistic zero-sum case. As in classical games, we introduce the concept of value, defined here as the set of plays a player can guarantee to improve upon, relative to their preference relation. We show that this set is recognized by an alternating parity automaton APW of polynomial size. We also establish the computational complexity of several problems related to the concepts of value and optimal strategy, taking advantage of the $ω$-automatic characterization of value. Next, we shift to multiplayer games and Nash equilibria, and revisit the threshold problem in this context. Based on an APW construction again, we close complexity gaps left open in the literature, and additionally show that cooperative rational synthesis is $\mathsf{PSPACE}$-complete, while it becomes undecidable in the non-cooperative case.

An Automata-Based Approach to Games with $ω$-Automatic Preferences

TL;DR

This paper generalizes game-theoretic analysis on graphs to -automatic preferences, where each player's objective is specified by a -automatic relation accepted by a deterministic parity automaton. The authors define a generalized value as the set of plays a player can guarantee to improve upon and show this set is -regular, recognizable by a polynomial-size alternating parity automaton, enabling automata-based solutions for threshold problems, Nash equilibria, and rational synthesis. They obtain tight complexity results: the threshold problem and NE existence are -complete; cooperative rational synthesis is -complete while non-cooperative rational synthesis is undecidable; Pareto-optimal NE outcomes exist with membership and -hardness. The results provide a unified automata-theoretic framework for reasoning about arbitrary -automatic preferences and have implications for verification and synthesis of reactive systems. The paper also outlines future directions, including robust equilibrium refinements (e.g., subgame-perfect equilibria) and extensions beyond -automatic to broader rational relations.

Abstract

This paper studies multiplayer turn-based games on graphs in which player preferences are modeled as -automatic relations given by deterministic parity automata. This contrasts with most existing work, which focuses on specific reward functions. We conduct a computational analysis of these games, starting with the threshold problem in the antagonistic zero-sum case. As in classical games, we introduce the concept of value, defined here as the set of plays a player can guarantee to improve upon, relative to their preference relation. We show that this set is recognized by an alternating parity automaton APW of polynomial size. We also establish the computational complexity of several problems related to the concepts of value and optimal strategy, taking advantage of the -automatic characterization of value. Next, we shift to multiplayer games and Nash equilibria, and revisit the threshold problem in this context. Based on an APW construction again, we close complexity gaps left open in the literature, and additionally show that cooperative rational synthesis is -complete, while it becomes undecidable in the non-cooperative case.
Paper Structure (6 sections, 10 theorems, 1 equation, 6 figures)

This paper contains 6 sections, 10 theorems, 1 equation, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Two-Player Zero-Sum Games
  4. Nash Equilibria
  5. Rational Synthesis
  6. Conclusion

Key Result

Lemma 5

Let $\mathcal{G}$ be a game and $v_0 \in V$ be a vertex. Then, the value $\mathsf{Val}_1(v_0)$ is accepted by an APW $\mathcal{B}$ with $|V|^2 \cdot |\mathcal{A}|$ states and a priority function of index $|\alpha|$.

Figures (6)

  • Figure 1: A DPW accepting the relation $\mathrel{\ltimes}$ for min-cost-reachability with target $T$.
  • Figure 2: A DPW accepting the relation $\mathrel{\ltimes}$ for max-reward reachability.
  • Figure 3: A DPW accepting the relation $\mathrel{\ltimes}$ for the combination of two Boolean reachability objectives.
  • Figure 4: An arena with round (resp. square) vertices owned by player $1$ (resp. player $2$).
  • Figure 7: The arena $A$ used in the undecidability result of \ref{['thm:crs-pspace-ncrs-undec']}.
  • ...and 1 more figures

Theorems & Definitions (17)

  • Example 1
  • Definition 3
  • Example 4
  • Lemma 5
  • Theorem 6
  • Theorem 7
  • Remark 8
  • Proposition 9
  • Remark 10
  • Lemma 12
  • ...and 7 more