Title: Theory / Unimportant / CS / Fundamental / Automata / Infinite / Infinite Duration Games Played on Graphs
Tags: récupéré hasNotNewEffectReturnsMeaning TypToValue closed complexity computer_to_instruction fromAlgorithm fromMath hasSeenConjDef mathToSee mid1516974248815 toUnary

Name: A tail objective
Definition: A set \(S\subseteq V^\omega\) such that for all \(\pi\), \(\pi\cdot\rho\in S\) iff \(\rho\in S\)
Variables: \(V\) a set of vertices

Name: A positional strategy
Definition: A strategy \(\lambda\) such that \(last(\pi)=last(\pi')\) implies \(\lambda(\pi)=\lambda(\pi')\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph
Name2: A memoryless strategy

Name: The set of memoryless strategy for player \(i\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph
Notation: \(\Lambda^{ml}_i\)

Name: A persistent strategy
Definition: A strategy \(\lambda\) such that \(last(\pi)=last(\pi')\) and \(\pi\preceq\pi'\) implies \(\lambda(\pi)=\lambda(\pi')\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph

Name: The set of persistent strategy for player \(i\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph
Notation: \(\Lambda^{p}_i\)

Name: The size of the strategy
Definition: \(|M|\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\langle M,Init,\delta,\lambda\rangle\) a finite memory strategy

Name: A spoiling of Player \(3-i\) against \(\lambda_i\) for \(Win_i\)
Definition: A strategy \(\lambda_{3-i}\) such that \(Out^v_G(\lambda_1,\lambda_2)\not\in Win_i\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(Win_i\) a winning condition
Let \(\lambda_i\) a strategy for player \(i\)

Name: The winning set for player i
Definition: The set of states from which player \(i\) has a winning strategy.
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(Win_i\) a winning condition
Notation: \(\langle\langle i\rangle\rangle(Win_i)\)

Name: The Player-1 attractor
Definition: The limit of the \(R_i\)'s
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(T\subseteq V\) a winning condition
Notation: \(Attr_1(T,G)\)

Definition: \(T\) if \(i=0\), otherwise:
-elements of \(R_{i-1}\)
-the elements of \(V_1\) with a successor in \(R_{i-1}\),
-the elements of \(V_2\) whose all successors belong to \(R_{i-1}\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(T\subseteq V\) a winning condition
\(i\in\mathbb N\)
Notation: \(R_i\)

Name: The memoryless attractor strategy
Definition: A function associating to each \(v\) of rank \(i\) a successor in \(R_{i-1}\), and an arbitrary value to each other elements.
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(T\subseteq V\) a winning condition
Property: Winning strategy for \(Attr_1(T,G)\)

Name: The rank of \(v\)
Definition: The least \(i\) such that \(v\in R_i\) if it exists, \(\infty\) otherwise
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(T\subseteq V\) a winning condition,
\(v\in V\)

Name: A trap for Player 1
Definition: for all \(v\in C\cap V_1\), \(Succ(v)\subseteq C\),
Variables: \(G=((V,E),V_1,V_2)\) a game graph
Definition2: for all \(v\in C\cap V_2\), we have \(Succ(v)\cap C\ne\emptyset\)
Conjdef: equivalently
DefType: A set \(C\subseteq V\)

Question: The complement of the attractor for player 1 is
Answer: a trap for Player 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph.
\(T\subseteq V\)

Name: A memoryless trap strategy
Definition: A strategy for player 2 such that, each \(v\in C\) is sent to an element of \(C\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph.
\(C\subseteq V\) a trap for player 1
Index: , 5
Kind: , Lem
Typ: A winning strategy for Player 2 for \(safe(C)\) for all vertices \(v\in C\)

Name: A simple cycle
Definition: A sequence \(v_0\dots v_n\) with \(v_0=v_n\), \(v_i\ne v_j\) for \(0<i<j\le n\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph

Name: \(\pi\) is a simple cycle
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\pi=v_0\dots v_n\)
Notation: \(\mathrm{Cy}(\pi)\)

Name: The set of simple cycles of \(G\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
Notation: \(\mathrm{Cycles}(G)\)

Definition: If \(\pi\) is a single state \(v\), then the empty set.
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\pi\) a finite path
Notation: \(\mathrm C(\pi)\)
Definition2: If \(\beta(\pi)\) is of the form \(\beta(\pi')=\pi_1\cdot v\cdot\pi_2\cdot v\), then \(\mathrm C(\pi_1\cdot v\cdot\pi_2); v\cdot\pi_2\cdot v\)
Conjdef: Either
Definition3: If \(\beta(\pi)\) is of the form \(\pi'\cdot v\) with \(v\not\in\pi'\), then \(\mathrm C(\pi')\)
Typ: A sequence of simple cycle

Definition: If \(\pi\) is a single state \(v\), then it is \(v\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\pi\) a finite path
Notation: \(\mathrm C(\pi)\)
Definition2: If \(\beta(\pi)\) is of the form \(\beta(\pi')=\pi_1\cdot v\cdot\pi_2\cdot v\), then \(\pi_1\cdot v\)
Conjdef: Either
Definition3: If \(\beta(\pi)\) is of the form \(\pi'\cdot v\) with \(v\not\in\pi'\), then \(\beta(\pi')\cdot v\)
Typ: A sequence of simple cycle

Smaller0: \(\bigcup_{i\in\mathbb N}\{v\mid v\in\beta(\pi(0\dots i))\}\)
Greater0: \(visit(\rho)\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\rho\) an infinite path
Index: 2
Kind: Prop
Smaller to greater: =

Definition: The set of cycles that appear infinitely many times in the cycle decomposition of \(\rho\).
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\rho\) an infinite path
Notation: \(\mathrm C^\omega(\rho)\)
Index: 2
Kind: Prop

Smaller0: \(\mathrm{inf}(\rho)\)
Greater0: \(\bigcup_{c\in C}\mathrm{visit}(c)\) with \(C\) the set of cycles \(c\) such that there exists infinely many positions \(i\in\mathbb N\) such that \(c\) is added to \(C(\rho(0\dots i))\)
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\rho\) an infinite path
Index: 3
Kind: Prop
Smaller to greater: =

Smaller0: \(v\in V\setminus \mathrm{Attr}_1(T,G)\)
Greater0: there is a memoryless winning strategy for Player 2 for the safety objective \(\mathrm{Win}_2\) for \(v\)
Page: 27
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(T\subseteq V\) a winning condition,
\(v\in V\)
Index: 6
Kind: Lem

Smaller0: \(\langle\langle 1\rangle\rangle(\mathrm{reach}(T))\)
Greater0: \(\mathrm{Attr}_1(T,G)\)
Page: 27
Variables: \(G=((V,E),V_1,V_2)\) a game graph
\(T\subseteq V\) a winning condition
Index: 4
Kind: Theo
Smaller to greater: =

Smaller0: \(\langle\langle 2\rangle\rangle(\mathrm{safe}(V\setminus T))\)
Greater0: \(V\setminus\langle\langle 1\rangle\rangle(\mathrm{reach}(T))\)
Page: 27
Variables: \(G=((V,E),V_1,V_2)\) a game graph
\(T\subseteq V\) a winning condition
Index: 4
Kind: Theo
Smaller to greater: =

Page: 27
Section: 2
Chapter: 4
Space complexity: NLOGSPACE-complete
Extra: problem
Effect: Reachability in directed graph

Page: 27, 30
Implementation: c:Array of V to int
Queue, Done, P: subset of V
Queue is initialized to T
Done to empty set
c initialized to 0
While v in Queue:
for each v' predecessor of v:
c[v'] is incremented
if (v' in V_1 and not in Done) or (c[v'] is the number of successors of v'):
_ add v' to Queue and Done
Section: 2
Chapter: 4
Effect: Computes the set of attractors for
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(T\subseteq V\) a winning condition,
Time complexity: Linear-time
PTIME-complete

Name: A monotonic function
Definition: A function \(f:2^V\to2^V\) such that \(A\subseteq B\subseteq V\) implies \(f(A)\subseteq f(B)\)
Page: 34
Chapter: 4
Section: 4.1
Variables: \(V\) a set,
Index: 23
Kind: Def

Name: A fixpoint of \(f\)
Definition: A set \(X\subseteq V\) such that \(f(X)=X\)
Page: 34
Chapter: 4
Section: 4.1
Variables: \(V\) a set,
\(f:2^V\to2^V\) a monotonic functions
Index: 23
Kind: Def

Name: A least fixpoint of \(f\)
Definition: A fixpoint of \(f\) included in each fixpoints of \(f\)
Page: 34, 37
Chapter: 4
Section: 4.1
Variables: \(V\) a set,
\(f:2^V\to2^V\) a monotonic functions
Notation: \(\mu X. h(X)\)
Index: 23
Kind: Def

Name: A greatest fixpoint of \(f\)
Definition: A fixpoint of \(f\) containing each fixpoint of \(f\)
Page: 34, 37
Chapter: 4
Section: 4.1
Variables: \(V\) a set,
\(f:2^V\to2^V\) a monotonic functions
Notation: \(\nu X. h(X)\)
Index: 23
Kind: Def

Name: The complement of \(f\)
Definition: \(X\mapsto V\setminus f(V\setminus X)\)
Page: 35
Chapter: 4
Section: 4.1
Variables: \(V\) a set,
\(f:2^V\to2^V\) a monotonic functions
Notation: \(\bar f\)
Index: 25
Kind: Def

Name: The set of monotic function
Page: 35
Section: 4.1
Chapter: 4
Index: 9
Variables: \(V\) a set,
Kind: Lem
Under: complement

Smaller0: \(\bar X\)
Greater0: the least fixed-point of \(\bar f\)
Page: 35
Chapter: 4
Section: 4.1
Variables: \(V\) a set,
\(f:2^V\to2^V\) a monotonic functions
Let \(X\) the least fixed point of \(f\)
Index: 7
Kind: Theo
Smaller to greater: is

Definition: The function sending \(X\subseteq V\) to the set of \(v\in V_i\) such that \(\mathrm{Succ}(v)\) intersects \(X\), and of \(v\in\mathrm{V}_{3-i}\) such that \(\mathrm{Succ}(v)\) is a subset of \(X\)
Page: 36
Section: 4.2
Chapter: 4
Variables: \(G=((V,E),V_1,V_2)\) a game graph
Notation: \(\mathrm{CPre}_i\)
Name: The one-step controllable predecessor operator for player \(i\)
Index: , Lem
Kind: , 10
Monotonic: Monotone

Smaller0: \(\mathrm{CPre}_i(\bar X)\)
Greater0: \(V\setminus\mathrm{CPre}_{3-i}(X)\)
Page: 36
Chapter: 4
Section: 4.2
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(X\subseteq V\),
\(i\in\{1,2\}\)
Smaller to greater: =

Smaller0: [$]\llangle 1\rrangle (reach(T))[/$]
Greater0: \(\mu X.T\cup \mathrm{CPre}_1(X)\)
Page: 38
Chapter: 4
Section: 4.2
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(T\subseteq V\)
Index: 8
Kind: Theo
Smaller to greater: =

Definition: \(((U,E\cap (U\times U)),U\cap V_1,U\cap V_2)\)
Page: 38
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(U\subseteq V\)
Notation: \(G\upharpoonright U\)

Name: A subgame of \(G\)
Definition: \(G\upharpoonright U\), for some \(U\subseteq V\), assuming that for each vertices in \(U\) there is at least one outgoing edge in \(U\)
Page: 38
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph

Smaller0: \(U\) is a trap
Greater0: \(G\upharpoonright U\) is a subgame of \(G\)
Page: 38
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph

Name: The core of \(\lambda_i\)
Definition: \(X\)
Page: 40
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(X\subseteq V\)
\(\lambda_i\) a strategy for player \(i\), on the set \(X\)
Context: Game graph

Name: A dont care vertex
Definition: A vertex not in \(X\)
Page: 40
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(X\subseteq V\)
\(\lambda_i\) a strategy for player \(i\), on the set \(X\)

Name: Their combined strategy
Definition: [$]\defFun{\bigcup_{j}X_j}{V}{v}{\lambda^j_i(v)\text{ when }v\in X_j}[/$]
Page: 40
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\((X_j)_{j\in[1,n]}\subseteq V\)
\((\lambda_i^j)_{j\in[1,n]}\) a strategy for player \(i\), on the set \(X_j\)
Assuming: \(X_j\)'s are disjoint

Smaller0: there is a memoryless strategy \(\lambda^U_2\) with \(U\) as its core that ensures the objective \(\mathrm{coBuchi}(\bar B)\) against all strategies of Player 1 for all vertices in \(U\)
Greater0: there is a memoryless strategy \(\lambda_2\) with \(U\cup \mathrm{Attr}_2(X,\bar G)\) as its core, that ensures the objective \(\mathrm{coBuchi}(\bar B)\) against all stratiegies of Player 1 for all vertices in this core
Page: 41
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(B,U,X\subseteq V\),
\(\bar G=G\upharpoonright(V\setminus U)\)
Index: 15
Kind: Lem
Smaller1: \(\bar G\) is a subgame, and \(X\) is a trap for Player 1 in \(\bar G\)

Smaller0: \(Z\) is a trap for player 2
Greater0: [$]Z\subseteq\llangle 1\rrangle(\mathrm{Buchi}(B))[/$]
Page: 41
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(B,Z\subseteq V\),
Index: 16
Kind: Lem
Smaller1: \(Z=\mathrm{Attr}_1(Z\cap B,G\upharpoonright Z)\)

Question: The complexity of deciding whether [$]v\in\llangle 1\rrangle(\mathrm{Buchi}(B))[/$] is
Answer: PTIME-complete
Page: 41
Chapter: 5
Section: 1
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(v\in V\),
\(T\subseteq V\)

Name: The set of outedges of \(u\)
Page: 47
Variables: \(G=(V,E)\) a graph,
\(u\in V\)
Abbreviation: \(\mathrm{Out}(u)\)

Name: An outgoing edge of \(u\)
Definition: A pair \((u,v)\in E\)
Page: 47
Variables: \(G=(V,E)\) a graph,
\(u\in V\)
Name2: An outedge of \(u\)

Name: The outdegree of \(u\)
Definition: The cardinal of \(\mathrm{Out}(u)\)
Page: 47
Variables: \(G=(V,E)\) a graph,
\(u\in V\)
Abbreviation: \(\mathrm{OutDeg}(u)\)
Extra: jump to next session

Definition: \(p^{-1}(i)\)
Page: 57
Variables: \(G=((V,E),V_1,V_2)\) a game graph
\(p:V\to\mathbb N\) a parity function,
\(i\in\mathbb N\)
Notation: \(P_i\)

Name: A player \(2\) graph
Definition: A game graph such that at each state, player 1 has only one choice
Page: 57

Definition: \(G\), where the only successor of \(v_1\in V_1\) is \(\lambda(v_1)\)
Page: 57
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(\lambda_1\) a strategy
Notation: \(G_{\lambda_1}\)
Denoted by: A player 2 graph

Question: Assumptions on parity game ?
Answer: \(P_0\cup P_1\ne\emptyset\),
Page: 58

Question: What can be said of a parity game with priorities 1 and 2 ?
Answer: Its equivalent to coBüchi automaton.
Page: 58

Question: What can be said of a parity game with priorities 0 and 1 ?
Answer: Its equivalent to Büchi automaton.
Page: 58

Smaller0: \(X\) is a trap for \(1\)
Greater0: \(Y\) is winning for \(2\) is \(G\)
Page: 60
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(Y\subseteq X\subseteq V\)
Index: 27
Kind: Lem
Smaller1: \(Y\) is winning for \(2\) is \(G\upharpoonright X\)

Smaller0: Player 2 has a memoryless strategy in states of \(Z\) with \(Z\) ats its core
Greater0: Player 2 has a memoryless strategy in states of \(Attr_2(Y,G\upharpoonright(V\setminus Z))\cup Z\) with this set at its core
Page: 60
Variables: \(G=((V,E),V_1,V_2)\) a game graph,
\(Y\subseteq Z\subseteq V\)
Index: 28
Kind: Lem
Smaller1: Player 2 has a memoryless strategy in states of \(Y\), in \(G\upharpoonright(V\setminus Z)\) with \(Y\) ats its core