Games with $ω$-Automatic Preference Relations

TL;DR

This work introduces a general automata-based framework for studying Nash equilibria in multi-player turn-based graph games, where each player's preferences are captured by $ω$-automatic relations realized by deterministic parity automata. It unifies qualitative ω-regular objectives and diverse quantitative reward models, and it analyzes fundamental decision problems: NE checking ($PSPACE$-complete), NE-outcome checking ($NP \cap coNP$ and parity-hard), NE existence (exponential in the arena size, automata, and priorities), and constrained NE existence (doubly exponential in priority counts). A key methodological advance is the reduction to a three-player game with imperfect information, which provides modular, scalable solutions and guarantees finite-memory equilibria when an NE exists. The results also identify tractable conditions under which NE existence is guaranteed, notably when preference relations are ω-recognizable preorders. Overall, the framework broadens the study of equilibria beyond specific reward functions and supports modular reasoning for reactive synthesis and equilibrium analysis in complex systems.

Abstract

This paper investigates Nash equilibria (NEs) in multi-player turn-based games on graphs, where player preferences are modeled as $ω$-automatic relations via deterministic parity automata. Unlike much of the existing literature, which focuses on specific reward functions, our results apply to any preference relation definable by an $ω$-automatic relation. We analyze the computational complexity of determining the existence of an NE (possibly under some constraints), verifying whether a given strategy profile forms an NE, and checking whether a specific outcome can be realized by an NE. When a (constrained) NE exists, we show that there always exists one with finite-memory strategies. Finally, we explore fundamental properties of $ω$-automatic relations and their implications for the existence of equilibria.

Figures (10)

• Figure 1: DPAs accepting preference relations, corresponding respectively to reachability, Büchi, and max-reward-reachability objectives. The priorities are indicated inside each state, and an edge label $T$, $\neg T$, or $*$ means that there is an edge for each label $v \in T$, $v \in V \setminus T$, and $v \in V$, respectively.
• Figure 2: An arena with round (resp. square) vertices owned by player $1$ (resp. player $2$).
• Figure 4: The game $\mathcal{G}$ and the DPA $\mathcal{A}_1$ accepting $\prec_{1}$ for the reduction of \ref{['theorem:OutcomeCheck']}.
• Figure 5: An illustration of the $\mathbb{P}_{1}$$\mathbb{C}$$\mathbb{P}_{2}$ game intuition: $\mathbb{P}_{1}$ observes the left part of a vertex (all $v,v',v"$), while $\mathbb{C}$ and $\mathbb{P}_{2}$ represent the deviating player $j$ and the coalition $-j$ in the right part (all $u,u'$). Given $\rho=vv'v"\dots$ and $\rho'=vuu'\dots$, $\mathbb{P}_{1}$ and $\mathbb{P}_{2}$ aim to ensure $\rho \not\prec_{j} \rho'$.
• Figure 6: An arena with one player.

Theorems & Definitions (26)

• Example 1
• Example 2
• Theorem 3: restate=nashchecking,name=
• Theorem 4
• Theorem 5: restate=NEexistenceGeneral,name=
• Theorem 6: restate=constrainedNEexistenceGeneral,name=
• Theorem 7: restate=correspondence,name=
• Corollary 8
• Proposition 9: restate=propertiesrelations,name=
• Proposition 10: restate=recognizablefiniteindex,name=