AGV 11.1 -- Infinite Games (Basic Definitions)

Notes > UdS AGV

Created At : 2025-02-11 17:11

Count:1.4k Views :

Introduction
Basic Definitions
Conclusion

Previous chapter: From semi-deterministic Büchi to deterministic Muller

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Introduction

We now introduce infinite two-player games on finite graphs. Infinite games are useful to solve the synthesis problem, where we are interested in finding a strategy that guarantees that a given specification is satisfied (cf. Section 1.2). As we will see, games also play a fundamental role in automata theory, in particular for automata over infinite trees.

Basic Definitions

The game is played on a graph, called the arena. The vertices of the graph are called positions and are partitioned into the positions of Player 0 and the positions of Player 1.

A play of the game starts in some initial position
In any positions, the player who owns the position chooses the edge on which the play is continued.
Player 0 wins if the play is an element of the winning condition.

The winner is determined by a winning condition, which, like the acceptance condition of an automaton on infinite words is a subset of the infinite words over the positions.

$\textbf{Definition 11.1. } \text{A }\textit{game arena}\text{ is a tuple }\mathcal{A} = (V,V_0,V_1,E)\text{, where}\newline\begin{array}{l}
\hspace{0.5cm} \cdot \ V_0\text{ and }V_1=V\setminus V_0\text{ are disjoint sets of positions,}\newline
\hspace{1cm} \text{called the positions of Player 0 and Player 1.}\newline
\hspace{0.5cm} \cdot \ E\subseteq V\times V\text{ is a set of edges such that every position }v\in V\newline
\hspace{1cm} \text{has at least one outgoing edge }(v,v’)\in E.\newline
\end{array}$

$\textbf{Definition 11.2. } \text{A }\textit{play}\text{ is an infinite sequence } \rho\in V^\omega\text{ such that}$
$$\forall n\in\mathbb{N}.(\rho(n),\rho(n+1))\in E$$

We say a play $\rho$ starts in a position $v$ iff $v=\rho(0)$. We denote the set of all possible plays on $\mathcal{A}$ with $\text{Plays}(\mathcal{A})$ and the set of all possible plays starting in position $v$ with $\text{Plays}(\mathcal{A},v)$.

$\textbf{Definition 11.3. }\text{A }\textit{game }\mathcal{G}=(\mathcal{A},\text{Win})\text{ consists of an arena }\mathcal{A}\text{ and a }\textit{winning condition}\newline\text{Win}\subseteq V^\omega\text{. We call a play }\rho\textit{ winning for Player 0}\text{ iif }\rho\in\text{Win and }\textit{winning for Player 1}\text{ otherwise.}$

When it is Player $i$’s turn, the current vertex must be a position of Player $i$ ($V_i$), all the prefix of the play seen so far (including current vertex) is called the history of the play, which is an element of $V^\ast V_i$.

A strategy fixes the decisions of a player based on the history of the play. A strategy for Player $i$ is a function $\sigma:V^\ast V_i\rightarrow V$ that selects for each such history a successor position.

$\textbf{Definition 11.4. }\text{A }\textit{strategy}\text{ for Player }i\text{ is a function }\sigma:V^\ast V_i\rightarrow V\text{ such that }(v,v’)\in E\newline\text{whenever }\sigma(wv)=v’\text{ for some }w\in V^\ast,v\in V_i$

In the following, we will use $\sigma$ and $\tau$ to denote strategies for some Player $i$ and the opponent Player $(1−i)$, respectively.

$\textbf{Definition 11.5. }\text{A play }\rho\text{ is }\textit{consistent}\text{ with a strategy }\sigma\text{ iff}$
$$\forall n\in\mathbb{N}.\text{if }\rho(n)\in V_i\text{ then }\rho(n+1)=\sigma(\rho[n])$$

We denote the set of all plays that begin in some position $v$ and are consistent with strategy $\sigma$ with $\text{Plays}(\mathcal{A}, \sigma, v)$. Note that the strategies $\sigma$ and $\tau$ of the two players together uniquely identify a specific play: $\mid \text{Plays}(\mathcal{A}, \sigma, v)\cap \text{Plays}(\mathcal{A}, \tau, v)\mid = 1$.

Our definition of a strategy is very general in the sense that the decisions are based on the entire history of the play. Intuitively, this means that the players have infinite memory. It often suffices to work with simpler strategies, such as memoryless strategies. Memoryless strategies are often also called positional.

$\textbf{Definition 11.6. }\text{A strategy }\sigma\text{ for Player }i\text{ is }\textit{memoryless}\text{ iff }\sigma(wv)=\sigma(v)\text{ for all }w\in V^\ast,v\in V_i.$

In a slight abuse of notation, memoryless strategies are often given directly as a function $\sigma:V_i\rightarrow V$ that maps the positions owned by Player $i$ to their successor positions. Next, we characterize winning strategies:

$\textbf{Definition 11.7. }\text{A strategy }\sigma\text{ for Player }i\text{ is }\textit{winning}\text{ from a position }v\text{ if all plays that}\newline\text{start in }v\text{ and that are consistent with }\sigma\text{ are winning for Player }i.$

Note that this definition refers to a specific position $v$ in which we start the play. The set of all positions where the player has a winning strategy is called the winning region.

$\textbf{Definition 11.8. }\text{ The }\textit{winning region }W_i(\mathcal{G})\text{ of Player }i\text{ in a game }\mathcal{G}\text{ is defined as}\newline\text{the set of positions }v\in V\text{ for which there exists a strategy for Player }i\text{ that is winning from }v.$

Note that the strategies for different positions in the winning region may be different. If a strategy $\sigma$ is winning from all positions of the winning region, we call $\sigma$ a uniform winning strategy.

It is easy to see that no position can be in the winning regions of both players. Suppose that there exists a position $v$ and strategies $\sigma$ and $\tau$ that are winning from $v$ for Player 0 and 1, respectively. Then the unique play that is consistent with $\sigma$ and $\tau$ would need to be both in Win, because $\sigma$ is winning, and not in Win, because $\tau$ is winning.

A more difficult question is whether all positions are in some winning region, i.e., whether the winning regions form a partition of $V$. This property is called the determinacy of a game:

$\textbf{Definition 11.9. }\text{A }\textit{game }\mathcal{G}\text{ is }\textit{determined }\text{if }V=W_0(\mathcal{G})\cup W_1(\mathcal{G})$

If the winning strategies are in fact memoryless, we say that the game is memoryless (also: positionally) determined.

$\textbf{Definition 11.10. }\text{A game is }\textit{memoryless determined }\text{if for every position }v\in V\text{, there exists}\newline\text{a memoryless stratey that is winning for some player from position }v.$

Conclusion

In this section, we have learned:

Arena: the graph of the game, expressed as a tuple $\mathcal{A}=(V,V_0,V_1,E)$
- Position: vertex of Arena $v\in V$
- Positions of Player $i$: a disjoint set of position $V_i$
Play: an infinite sequence of $\rho\in V^\omega$
- set of all Plays: $\text{Plays}(\mathcal{A})$
- set of all Plays in position $v$: $\text{Plays}(\mathcal{A},v)$
- starting position: $v = \rho(0)$
- the player who owns the position chooses the edge on which the play is continued ($\rho\in V_i$)
Game: consist of an arena and a winning condition $\mathcal{G}=(\mathcal{A},\text{Win})$
- winning condition: $\text{Win}\subseteq V^\omega$
- winning play for Player 0: $\rho\in\text{Win}$
- winning play for Player 1: $\rho\notin\text{Win}$
history: all previous positions $V^\ast$
Strategy: decisions of a player based on history of the play
- Strategy of Player $i$: $\sigma:V^\ast V_i\rightarrow V$
- Strategy of Player 0: $\sigma$
- Strategy of Player 1: $\tau$
Memoryless (positional) Strategy: $\sigma(wv)=\sigma(v)\text{ for all }w\in V^\ast,v\in V_i$
Winning Region: set of all positions that Player $i$ has a winning strategy $W_i(\mathcal{G})\in V$
- Uniform Winning Strategy: one strategy that can apply to any position in a winning region.
Determinacy: $\mathcal{G}$ is determined if every position is in some player’s winning region $V=W_0(\mathcal{G})\cup W_1(\mathcal{G})$
- A determined game have winning strategy in every positions.
Memoryless Game: all strategies are memoryless in every position of a determined game

Next chapter: Reachability Games