Definition 1.1 (Syntax of Arithmetic Expression). The syntax of arithmetic expressions is defined as

where $/$ stands for integer division, $\%$ stands for mod. We add parentheses here to avoid the arithmetic priority issue, and will omit them later on.

The set of all arithmetic expressions is denoted by $\text{AExp}<!--\; FUNCTION\; APPLICATION\; -->$.

Definition 1.2 (Syntax of Boolean Expression). The syntax of a boolean expression is defined as

where $𝑒$ is an arithmetic expression.

The set of all arithmetic expressions is denoted by $\text{BExp}<!--\; FUNCTION\; APPLICATION\; -->$.

Definition 1.3 (Syntax of Program). The syntax of a program $𝑃$ is defined as

where $𝑥\in \text{Vars}<!--\; FUNCTION\; APPLICATION\; -->$, $𝑒$ is an expression, and $𝑃;𝑃$ means a sequence of two program.

Definition 1.4 (Valuation). A valuation is a function $𝑣:\text{Vars}<!--\; FUNCTION\; APPLICATION\; -->\to Z$, which specifies values of variables. The set of all valuations is denoted by $\text{Val}<!--\; FUNCTION\; APPLICATION\; -->$. Given a valuation $𝑣$, the value of the variable $𝑥$ is $𝑣(𝑥)$. During the execution of the program, the variable itself remains the same (just a name), but its value changes as the valuation changes.

Definition 1.5 (Semantics of Arithmetic Expression). The semantics of an expression $𝑒$ is the meaning / value of the expression, denoted by $[[𝑒]]$. Formally, $[[𝑒]]$ is a function $:\text{Val}<!--\; FUNCTION\; APPLICATION\; -->\to Z$ (not $[[·]]$), such that the value of function $[[𝑒]]$ at $𝑣$, denoted by $[[𝑒]](𝑣)$ or simply $[[𝑒]]𝑣$, is the value of expression $𝑒$ given the valuation $𝑣$.

Definition 1.6 (Semantics of Boolean Expression). The semantics of a Boolean expression $𝑏$ is a function $[[𝑏]]:\text{Val}<!--\; FUNCTION\; APPLICATION\; -->\to \{\mathsf{\text{true}}<!--\; FUNCTION\; APPLICATION\; -->,\mathsf{\text{false}}<!--\; FUNCTION\; APPLICATION\; -->\}$, such that $[[𝑏]](𝑣)$ is the truth value of $𝑏$ given a valuation $𝑣$.

Notation 1 (Inference-rule notation). $$ means that if the Assumptions are true, then the Result is true.

Definition 1.7 (State of Program). We can define the state of a program as:

1.

The current valuation: $𝑣:\text{Vars}<!--\; FUNCTION\; APPLICATION\; -->\to Z$.

2.

The current valuation together with a pointer showing the current position in code: $(𝑙,𝑣)$ where $𝑙$ is a line number.

3.

The current valuation together with a piece of remaining code to be executed: $(𝑃,𝑣)$.

We denote by $\mathrm{\Sigma }$ the set of all states. Program execution is simply captured by transitions between states.

Definition 1.8 (Operational Semantics). Operational semantics is a category of semantics that is defined by inference rules over transitions between states.

Definition 1.9 (Small-step Transition Relation). A samll-step transition relation $(𝑃,𝑣)\to ({𝑃}^{\prime },{𝑣}^{\prime })$ means that the first state transits to the second state in one execution step.

Definition 1.10 (Small-step Operational Semantics). Small-step operational semantics defines inference rules for single-step transitions.

Definition 1.11 (Transitive closure). $(𝑃,𝑣){\to }^{\ast }({𝑃}^{\prime },{𝑣}^{\prime })$ means that starting from state $(𝑃,𝑣)$, we can reach state $({𝑃}^{\prime },{𝑣}^{\prime })$ in certain number of steps. Formally, it is defined by

Definition 1.12 (Termination). A program $𝑃$ with valuation $𝑣$ will terminate if it will eventually transit to an empty program, denoted by $\mathsf{\text{Term}}<!--\; FUNCTION\; APPLICATION\; -->(𝑃,𝑣)$. Formally, it is defined by

Definition 1.13 (Big-Step Relation). A big-step relation $(𝑃,𝑣)\downarrow {𝑣}^{\prime }$ means that the program $𝑃$ with valuation $𝑣$ terminates, modifyng the valuation to ${𝑣}^{\prime }$.

Definition 1.14 (Big-Step Operational Semantics). Big-step operational semantics defines inference rules for big-step relations.

Example 1.1. Consider $𝑃:𝑥=1$ and $𝑄:𝑥=0;\mathsf{\text{while}}<!--\; FUNCTION\; APPLICATION\; -->𝑥\ne 1\mathsf{\text{do}}<!--\; FUNCTION\; APPLICATION\; -->𝑥=1\ast \mathsf{\text{skip}}<!--\; FUNCTION\; APPLICATION\; -->\mathsf{\text{od}}<!--\; FUNCTION\; APPLICATION\; -->$. $𝑃$ always terminates with $𝑥=1$, but $𝑄$ terminates only when sometimes $𝑥=1$ is executed. We could not say they are equivalent.

Definition 1.15 (Denotational Semantics). Denotational semantics is a category of semantics that is defined as mathematical functions. Usually, the denotational semantics of a program is obtained inductively based on the (already defined) denotational semantics of its subprograms.

Definition 1.16 (Denotational Semantics of Program). The semantics of a program $𝑃$ is the function that transforms the initial state (valuation) to the final state (valuation), denoted by $[[𝑃]]$. Formally, it is a partial function $[[𝑃]]:\mathrm{\Sigma }\text{⇀}<!--\; FUNCTION\; APPLICATION\; -->\mathrm{\Sigma }$. It is partial because it is not defined on initial states that do not terminate, etc.

Definition 1.17 (Conditional statement). Let $𝑓,𝑔:\mathrm{\Sigma }\text{⇀}<!--\; FUNCTION\; APPLICATION\; -->\mathrm{\Sigma },𝑏:\mathrm{\Sigma }\to \{\mathsf{\text{true}}<!--\; FUNCTION\; APPLICATION\; -->,\mathsf{\text{false}}<!--\; FUNCTION\; APPLICATION\; -->\}$, then the conditional semantics $\mathsf{\text{cond}}<!--\; FUNCTION\; APPLICATION\; -->(𝑏,𝑓,𝑔):\mathrm{\Sigma }\text{⇀}<!--\; FUNCTION\; APPLICATION\; -->\mathrm{\Sigma }$ is defined as

Proposition 1.1. Given an boolean expression $𝑏$ and a program $𝑃$, there exists a fixed point of ${𝑇}_{𝑏,𝑃}$.

Proof 1.1. We prove by constructing functions based on Operational Semantics.

For any program $𝑃$ and valuation $\mathit{𝑣𝑎𝑙}$, we define $[[𝑃]]\mathit{𝑣𝑎𝑙}=\mathit{𝑣𝑎}{𝑙}^{\prime }$ iff $(𝑃,\mathit{𝑣𝑎𝑙})\mathit{\downarrow 𝑣𝑎}{𝑙}^{\prime }$ in Operational Semantics, and $[[𝑃]]\mathit{𝑣𝑎𝑙}=\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->$ if there is no such $\mathit{𝑣𝑎}{𝑙}^{\prime }$ (does not terminate).

Running the inference rules, we will get a function $𝑓$ for $[[\mathsf{\text{while}}<!--\; FUNCTION\; APPLICATION\; -->𝑏\mathsf{\text{do}}<!--\; FUNCTION\; APPLICATION\; -->𝑃]]$ and a function $𝑔$ for $[[\mathsf{\text{if}}<!--\; FUNCTION\; APPLICATION\; -->𝑏\mathsf{\text{then}}<!--\; FUNCTION\; APPLICATION\; -->𝑃;\mathsf{\text{while}}<!--\; FUNCTION\; APPLICATION\; -->𝑏\mathsf{\text{do}}<!--\; FUNCTION\; APPLICATION\; -->𝑃\mathsf{\text{else}}<!--\; FUNCTION\; APPLICATION\; -->\mathsf{\text{skip}}<!--\; FUNCTION\; APPLICATION\; -->\mathsf{\text{fi}}<!--\; FUNCTION\; APPLICATION\; -->]]$. Recall the corollary about the equivalence between two, which basically means

Thus, $𝑓=𝑔={𝑇}_{𝑏,𝑃}(𝑓)$. $𝑓$ is indeed a fixed point.

Proposition 1.2. The fixed point is not unique, but the least defined fixed point is unique.

Proof 1.2. We can prove the nonuniqueness simply by finding multiple fixed points: $𝑇(𝑓)=𝑓$ iff

So $𝑓$ could be $\mathsf{\text{cond}}<!--\; FUNCTION\; APPLICATION\; -->([[𝑏]],𝑐,[[\mathsf{\text{skip}}<!--\; FUNCTION\; APPLICATION\; -->]])$ for any constant function $𝑐$ ($\forall <!--\; FUNCTION\; APPLICATION\; -->\mathit{𝑣𝑎𝑙},𝑐(\mathit{𝑣𝑎𝑙})=𝑐$).

Proof 1.3. More detailed analysis of constraints on the fixed points: Let $𝑔$ be any fixed point of ${𝑇}_{𝑏,𝑃}$ (abbreviated to $𝑇$ below). Let $\mathit{𝑣𝑎}{𝑙}_0$ be an arbitraty initial valuation, then there are three possible cases of the while loop.

1.

The entire while loop terminates after a finite number, say $𝑛$, of iterations:

We have

$$\begin{array}{lll}\hfill \mathit{𝑣𝑎}{𝑙}_{𝑖+1}=[[𝑃]]\mathit{𝑣𝑎}{𝑙}_{𝑖}& & \hfill \text{(1)}\end{array}$$

for $𝑖=0,1,\dots ,𝑛-1$. Moreover,

$$\begin{array}{lll}\hfill [[𝑏]]\mathit{𝑣𝑎}{𝑙}_0=\cdots =[[𝑏]]\mathit{𝑣𝑎}{𝑙}_{𝑛-1}=\mathsf{\text{true}}<!--\; FUNCTION\; APPLICATION\; -->,[[𝑏]]\mathit{𝑣𝑎}{𝑙}_{𝑛}=\mathsf{\text{false}}<!--\; FUNCTION\; APPLICATION\; -->.& & \hfill \end{array}$$

This implies that

$$\begin{array}{llll}\hfill 𝑇(𝑔)(\mathit{𝑣𝑎}{𝑙}_{𝑖})& =\mathsf{\text{cond}}<!--\; FUNCTION\; APPLICATION\; -->([[𝑏]],𝑔◦[[𝑃]],[[\mathsf{\text{skip}}<!--\; FUNCTION\; APPLICATION\; -->]])(\mathit{𝑣𝑎}{𝑙}_{𝑖})& \hfill & \\ \hfill & =𝑔◦[[𝑃]](\mathit{𝑣𝑎}{𝑙}_{𝑖})=𝑔(\mathit{𝑣𝑎}{𝑙}_{𝑖+1})& \hfill \text{(2)}\end{array}$$

for $𝑖=0,\dots ,𝑛-1$, and $𝑇(𝑔)(\mathit{𝑣𝑎}{𝑙}_{𝑛})=[[\mathsf{\text{skip}}<!--\; FUNCTION\; APPLICATION\; -->]](\mathit{𝑣𝑎}{𝑙}_{𝑛})=\mathit{𝑣𝑎}{𝑙}_{𝑛}$. Since $𝑔$ is a fixed point,

$$\begin{array}{lll}\hfill 𝑔(\mathit{𝑣𝑎}{𝑙}_0)=𝑔(\mathit{𝑣𝑎}{𝑙}_1)=\cdots =𝑔(\mathit{𝑣𝑎}{𝑙}_{𝑛})=\mathit{𝑣𝑎}{𝑙}_{𝑛}.& & \hfill \text{(*1)}\end{array}$$

2.

Some iteration, say the $𝑛$-th one, does not terminate so the whole loop does not terminate.

Equation (1) still holds for $𝑖=0,\dots ,𝑛-1$. And we have

$$\begin{array}{lll}\hfill [[𝑏]]\mathit{𝑣𝑎}{𝑙}_0=\cdots =[[𝑏]]\mathit{𝑣𝑎}{𝑙}_{𝑛-1}=[[𝑏]]\mathit{𝑣𝑎}{𝑙}_{𝑛}=\mathsf{\text{true}}<!--\; FUNCTION\; APPLICATION\; -->.& & \hfill \end{array}$$

Then, equation (2) also holds for $𝑖=0,\dots ,𝑛-1$. Since $𝑔$ is a fixed point of $𝑇$,

$$\begin{array}{lll}\hfill 𝑔(\mathit{𝑣𝑎}{𝑙}_0)=\cdots =𝑔(\mathit{𝑣𝑎}{𝑙}_{𝑛}).& & \hfill \text{(*2)}\end{array}$$

3.

Every iteration terminates but the loop itself does not:

Equation (1) and $[[𝑏]]\mathit{𝑣𝑎}{𝑙}_{𝑖}=\mathsf{\text{true}}<!--\; FUNCTION\; APPLICATION\; -->$ holds for $𝑖=0,1,\dots$. Similarly, we have

$$\begin{array}{lll}\hfill 𝑔(\mathit{𝑣𝑎}{𝑙}_0)=𝑔(\mathit{𝑣𝑎}{𝑙}_1)=\mathit{\dots 𝑔}(\mathit{𝑣𝑎}{𝑙}_{𝑛})=\dots .& & \hfill \text{(*3)}\end{array}$$

Equations (*1), (*2), and (*3) are the only constraints we have on $𝑔$ in the three cases, respectively. In (*1) 1, the values $𝑔(\mathit{𝑣𝑎}{𝑙}_0),\dots ,𝑔(\mathit{𝑣𝑎}{𝑙}_{𝑛})$ are uniquely determined to be $\mathit{𝑣𝑎}{𝑙}_{𝑛}$. However, in (*2) and (*3), the values are not unique.

We want the $𝑔$ that aligns with the Operational Semantics. Requirements are:

• Case 2: $[[𝑃]]\mathit{𝑣𝑎}{𝑙}_{𝑛-1}\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->$ since it does not terminate. Thus, $𝑔(\mathit{𝑣𝑎}{𝑙}_{𝑛})=𝑇(𝑔)\mathit{𝑣𝑎}{𝑙}_{𝑛-1}=𝑔([[𝑃]]\mathit{𝑣𝑎}{𝑙}_{𝑛-1})=𝑔(\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->)$, which should be $\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->$. Hence, $𝑔(\mathit{𝑣𝑎}{𝑙}_0)=\cdots =𝑔(\mathit{𝑣𝑎}{𝑙}_{𝑛})=\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->$.
• Case 3: $𝑔(\mathit{𝑣𝑎}{𝑙}_0)=\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->$ since the while loop does not terminate. Thus, $𝑔(\mathit{𝑣𝑎}{𝑙}_0)=𝑔(\mathit{𝑣𝑎}{𝑙}_1)=\mathit{\dots 𝑔}(\mathit{𝑣𝑎}{𝑙}_{𝑛})=\cdots =\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->$.

Now, this $𝑔$ is uniquely determined.

Least defined fixed point: A fixed point such that at any initial valuation it is not uniquely determined, its value is $\mathsf{\text{undefined}}<!--\; FUNCTION\; APPLICATION\; -->$.

The $𝑔$ uniquely determined above is the least defined fixed point.

Definition 1.18 (Invariant). Assertion assigned to some point of the program that always hold whenever the program reach the point.

Definition 1.19 (Pre-conditon and post-conditon). The invariant that is assigned to the beginning or the end of a (part of) program, respectively.

Definition 1.20 (Hoare triple). A hoare triple $\{𝐴\}𝑃\{𝐵\}$, where $𝐴$ and $𝐵$ are two assertions and $𝑃$ is a program, means that, for any current $\mathit{𝑣𝑎𝑙}$, if $𝐴$ holds in state $\mathit{𝑣𝑎𝑙}$ (denoted by $\mathit{𝑣𝑎𝑙}\mathit{\models 𝐴}$), and $\mathit{𝑣𝑎}{𝑙}^{\prime }$ is a state that can be reached by a terminating run of $𝑃$ starting at $\mathit{𝑣𝑎𝑙}$, then $𝐵$ holds in state $\mathit{𝑣𝑎}{𝑙}^{\prime }$. Formally, $\{𝐴\}𝑃\{𝐵\}$ is defined as the logical statement

Definition 2.1. A game graph or arena is a finite directed graph $(𝑉,𝐸)$ with a partition $({𝑉}_1,{𝑉}_2)$ of $𝑉$, where

• ${𝑉}_1$ and ${𝑉}_2$ belong to the two players, respectively,
• every vertex has at least one out-going edge.

Given an initial vertex $𝑣\in 𝑉$, the game proceeds as follows:

• At a vertex $𝑣\in {𝑉}_{𝑖}$ player $𝑖$ transitions the state along of the out-edges of $𝑣$.
• An outcome is an infinite (by 2.1) path resulting from the game play.
• An objective for a player is a set of outcomes. The player wins if the outcome is in the objective.
• A game is zero-sum if the objective of one player is the complement of the objective of the other player.

Definition 2.2. Let $𝑇$ be a set of target vertices. Then,

• the (alternating) reachability objective is defined as $\text{Reach}<!--\; FUNCTION\; APPLICATION\; -->(𝑇)=\{𝜌:\text{Visit}<!--\; FUNCTION\; APPLICATION\; -->(𝜌)\cap 𝑇\ne \varnothing \}$, i.e., the set of outcomes that ever reach (some vertices of) $𝑇$. The problem of finding the initial vertices from which player 1 can win is called the (alternating) reachability game problem.
• The safety objective is defined as $\text{Safe}<!--\; FUNCTION\; APPLICATION\; -->(𝑇)=\{𝜌:\text{Visit}<!--\; FUNCTION\; APPLICATION\; -->(𝜌)\subseteq 𝑇\}$, i.e., the set of outcomes that only traverse within $𝑇$.

Definition 2.3. Let $𝑇$ be a set of Büchi vertices. Then,

• The Büchi objective is defined as $\text{Buchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑇)=\{𝜌:\text{inf}<!--\; FUNCTION\; APPLICATION\; -->(𝜌)\cap 𝑇\ne \varnothing \}$, i.e., the set of outcomes that visit (some vertices of) $𝑇$ infinitely many times.
• The coBüchi objective is defined as $\text{coBuchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑇)=\{𝜌:\text{inf}<!--\; FUNCTION\; APPLICATION\; -->(𝜌)\subseteq 𝑇\}$, i.e., the set of outcomes that visits vertices out of $𝑇$ only finitely many times (enter $𝑇$ at some time and then never leave $𝑇$).

Definition 2.4. Let $𝑝:𝑉\to \{0,1,\dots ,𝑑\}$ be a priority function. Then the parity objective is defined as $\text{parity}<!--\; FUNCTION\; APPLICATION\; -->(𝑝)=\{𝜌|\text{min}<!--\; FUNCTION\; APPLICATION\; -->\{𝑝(𝑣)|𝑣\in \text{inf}<!--\; FUNCTION\; APPLICATION\; -->(𝜌)\}\text{is even}\}$.

Proposition 2.1. $\text{Buchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑇)=\text{parity}<!--\; FUNCTION\; APPLICATION\; -->(𝑝)$ where $𝑝(𝑣)=0$ for $𝑣\in 𝑇$ and $𝑝(𝑣)=1$ otherwise.

Proposition 2.2. $\text{coBuchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑇)=\text{parity}<!--\; FUNCTION\; APPLICATION\; -->(𝑝)$ where $𝑝(𝑣)=2$ for $𝑣\in 𝑇$ and $𝑝(𝑣)=1$ otherwise.

Proposition 2.3. In general, $\text{parity}<!--\; FUNCTION\; APPLICATION\; -->(𝑝)=\overline{\text{parity}<!--\; FUNCTION\; APPLICATION\; -->(𝑞)}$ for $𝑞=1+𝑝$ (or $𝑞=2𝑘+1+𝑝$ for $𝑘\in Z$).

Definition 2.5. We say an objective $𝑂$ is a tail objective if whenever $𝜌\in 𝑂$, we have $𝜌[\mathit{𝑖\dots }]\in 𝑂$ for every $𝑖$.

Proposition 2.4. Parity objectives are tail objectives since finite prefix does not matter.

Notation 2. For a vertex $𝑣$, we denote by $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑢)=\{𝑢\in 𝑉:(𝑢,𝑣)\in 𝐸\}$ the set of successor vertices of $𝑢$.

Definition 2.6. A strategy for player $𝑖$ is a function ${𝜎}_{𝑖}:{𝑉}^{\ast }\times {𝑉}_{𝑖}\to 𝑉$, where ${𝑉}^{\ast }$ represents the history (the portion of path visited) domain. Given history $𝑤$ and current vertex $𝑣$, the strategy outputs Player $𝑖$’s chioce of the next vertex to visit ${𝜎}_{𝑖}(𝑤,𝑣)\in \text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)$.

• ${𝜎}_{𝑖}$ is called memoryless if it is only based on the current state: ${𝜎}_{𝑖}(𝑤,𝑣)={𝜎}_{𝑖}({𝑤}^{\prime },𝑣)$ for all $𝑤,{𝑤}^{\prime }\in {𝑉}^{\ast }$. In this case, we can denote ${𝜎}_{𝑖}:{𝑉}_{𝑖}\to 𝑉$.
• ${𝜎}_{𝑖}$ is called persistent if back to the same vertex it still makes the same decision: ${𝜎}_{𝑖}(𝑤,𝑣)={𝜎}_{𝑖}({𝑤}^{\prime },𝑣)$ for all paths $𝑤,{𝑤}^{\prime }$ such that $𝑤$ is a prefix of ${𝑤}^{\prime }$, denoted by $𝑤\le {𝑤}^{\prime }$.

Notation 3. The outcome is fixed given the initial vertex $𝑣$ and strategies (no matter memoryless or not) of the two players ${𝜎}_1,{𝜎}_2$. We denote it by $\text{Outcome}<!--\; FUNCTION\; APPLICATION\; -->(𝑣,{𝜎}_1,{𝜎}_2)$.

Remark 1. In the case where strategies have memory, one may discuss the size of the memory. The memory is said to be finite if it has finite bits (not that it can memorize finite number of steps).

Definition 2.7. A strategy ${𝜎}_1$ for player $1$ is called a winning strategy for player 1 from a vertex $𝑣$ if for every strategy ${𝜎}_2$ of player $2$ we have $\text{Outcome}<!--\; FUNCTION\; APPLICATION\; -->(𝑣,{𝜎}_1,{𝜎}_2)\in {𝑂}_1$. The winning strategies for player $2$ are defined analogously.

Definition 2.8 (Spoiling strategy). A strategy ${𝜎}_2$ for player $2$ spoils ${𝜎}_1$ if $\text{Outcome}<!--\; FUNCTION\; APPLICATION\; -->(𝑣,{𝜎}_1,{𝜎}_2)\notin {𝑂}_1$.

Definition 2.9. Given an objective ${𝑂}_{𝑖}$ for player $𝑖$, the winning set ${\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_{𝑖}({𝑂}_{𝑖})$ is the subset of vertices from which player $𝑖$ has a winning strategy (i.e., the other player has no spoiling strategy for this).

Definition 2.10. A game with objectives ${𝑂}_1,{𝑂}_2$ for players 1 and 2 respectively is determined if ${\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_1({𝑂}_1)=𝑉\backslash {\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_2({𝑂}_2)$.

Definition 2.11. Let $𝑇$ be a set of target vertices. The attractor for player $𝑖$ is defined as ${\text{Attr}<!--\; FUNCTION\; APPLICATION\; -->}_{𝑖}(𝑇)={\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_{𝑖}(\text{Reach}<!--\; FUNCTION\; APPLICATION\; -->(𝑇))$, the set of vertices from which player $𝑖$ has a strategy to reach $𝑇$.

Proposition 2.5. The set ${\text{Attr}<!--\; FUNCTION\; APPLICATION\; -->}_1(𝑇)$ can be inductively defined as follows:

• Base case ${𝐴}_0=𝑇$ (trivial)

• Inductive step: Assume ${𝐴}_{𝑖}$ is a subset of the attractor. Consider some initial vertex $𝑣$ that is not yet included.

  • If $𝑣$ belongs to Player 1 and has an edge towards ${𝐴}_{𝑖}$, then Player 1 can move the state along the and win.
  • If $𝑣$ belongs to Player 2 and has only edges towards ${𝐴}_{𝑖}$, then Player 1 can win too.

  Therefore, setting ${𝐴}_{𝑖+1}={𝐴}_{𝑖}\cup \{𝑣\in {𝑉}_1|\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\cap {𝐴}_{𝑖}\ne \varnothing \}\cup \{𝑣\in {𝑉}_2|\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\subseteq {𝐴}_{𝑖}\}$, ${𝐴}_{𝑖+1}$ is an extended subset of attractor. The process stops when ${𝐴}_{𝑖+1}=\varnothing$. Then, $𝐴={\cup }_{𝑖\ge 0}{𝐴}_{𝑖}$.

The inductive definition for ${\text{Attr}<!--\; FUNCTION\; APPLICATION\; -->}_2(𝑇)$ can be analogous.

Definition 2.12. For all vertices in ${\text{Attr}<!--\; FUNCTION\; APPLICATION\; -->}_1(𝑇)$, define $\text{rank}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)=𝑖$ if $𝑣\in {𝐴}_{𝑖}\backslash {𝐴}_{𝑖-1}$ (See Prop. 2.5).

Proposition 2.6. By definition, $𝐴\subseteq {\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_1(\text{Reach}<!--\; FUNCTION\; APPLICATION\; -->(𝑇))$ and $𝐴\cap {\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_2(\text{Safe}<!--\; FUNCTION\; APPLICATION\; -->(𝑉\backslash 𝑇))=\varnothing$.

Definition 2.13. Let $𝑇$ be a set of target vertices. A vertex set $𝐶\cap 𝑇=\varnothing$ is said to be trap for player 1 if player 2 has a strategy to confine the state in $𝐶$ (and hence never reaches $𝑇$), i.e.,

1.

If $𝑣\in 𝐶\cap {𝑉}_1$, then $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\subseteq 𝐶$

2.

If $𝑣\in 𝐶\cap {𝑉}_2$, then $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\cap 𝐶\ne \varnothing$.

We often use the term “a trap of player 1 in $𝐶$” or “a trap of player 1 out of $𝑇$”.

Proposition 2.7. $𝑉\backslash {\cup }_{𝑖\ge 0}{𝐴}_{𝑖}$ is a trap for player 1.

Proof 2.1.

1.

$𝑇\subseteq 𝐴⟹(𝑉\backslash 𝐴)\cap 𝑇=\varnothing$.

2.

Suppose $𝑣\in (𝑉\backslash 𝐴)\cap {𝑉}_1$. If $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\mathit{⊈𝑉}\backslash 𝐴$, i.e., $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\cap 𝐴\ne \varnothing$, then $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\cap {𝐴}_{𝑖}\ne \varnothing$ for some $𝑖$. In this case, $𝑣$ should have been added into $𝐴$, which is a contradiction. Thus, $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\subseteq 𝑉\backslash 𝐴$.

3.

Suppose $𝑣\in (𝑉\backslash 𝐴)\cap {𝑉}_2$. If $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\cap (𝑉\backslash 𝐴)=\varnothing$, i.e., $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\subseteq 𝐴$, then we can partition $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)$ to several sets such that each set $\subseteq {𝐴}_{𝑖}$ for some ${𝐴}_{𝑖}$. $𝑣$ should have been added into $𝐴$, which is a contradiction. Thus, $\text{Succ}<!--\; FUNCTION\; APPLICATION\; -->(𝑣)\cap (𝑉\backslash 𝐴)=\varnothing$.

Derivation 2.1. Together, we have $𝑉\backslash 𝐴\subseteq {\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_2(\text{Safe}<!--\; FUNCTION\; APPLICATION\; -->(𝑉\backslash 𝑇))$, and $(𝑉\backslash 𝐴)\cap {\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_1(\text{Reach}<!--\; FUNCTION\; APPLICATION\; -->(𝑇))=\varnothing$. This implies that

Proposition 2.8. $𝐴={\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_1(\text{Reach}<!--\; FUNCTION\; APPLICATION\; -->(𝑇))$ and $𝑉\backslash 𝐴={\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_2(\text{Safe}<!--\; FUNCTION\; APPLICATION\; -->(𝑉\backslash 𝑇))$.

Definition 2.14 (Subgame arena). Given an arena $𝐺=(𝑉,{𝑉}_1,{𝑉}_2,𝐸)$ and a set $𝑊\subseteq 𝑉$, if every vertex in $𝑊$ has a successor in $𝑊$, then the subgame arena at $𝑊$ is defined as ${𝐺}_{𝑊}=(𝑊,{𝑉}_1\cap 𝑊,{𝑉}_2\cap 𝑊,𝐸\cap 𝑊\times 𝑊)$ (remain edges within $𝑊$ only).

Proposition 2.9. Player 2 has a winning strategy (for $\text{coBuchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑉\backslash 𝑇)$) starting from $𝐶={\text{Attr}<!--\; FUNCTION\; APPLICATION\; -->}_2(𝐵)$, and hence player 1 does not have a winning strategy from the set. ($𝐶\subseteq {\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_2({𝑂}_2)$).

Proof 2.2.

• Player 2 first plays the strategy that reaches $𝐵$. During this process, the path can only reach $𝑇$ finitely many times.
• Then play the strategy that stays in $𝐵$.
• Since $𝐵\cap 𝑇=\varnothing$, the outcome visits $𝑇$ only finitely many times.

Proposition 2.10. The following algorithm finds ${\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_2(\text{coBuchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑉\backslash 𝑇))$ and ${\text{Win}<!--\; FUNCTION\; APPLICATION\; -->}_1(\text{Buchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑉\backslash 𝑇))$: Mark all vertices in $𝐶$ as winning for Player 2, and recursively solve the subgame at $𝑉\backslash 𝐶$ with objective ${𝑂}_1=\text{Buchi}<!--\; FUNCTION\; APPLICATION\; -->(𝑇\backslash (𝑇\cap 𝐶))$. Formally: