add example Büchi Game

This commit is contained in:
Yu Cong 2024-10-05 10:05:02 +08:00
parent 80e76bb505
commit d507c8ba55
4 changed files with 182 additions and 48 deletions

View File

@ -1,6 +1,5 @@
\definecolor{lightblue}{rgb}{0.67,0.87,0.9}
%------------------------------------------------
\section{Motivation \& References}
%------------------------------------------------
@ -91,7 +90,7 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
$R_i:=\{v\in V|$ P0 can force a visit from v to a vertex in $T$ in i steps$\}$\\~
Define Reachability set of $T$ for P0, $Reach(T,0) := \bigcup_{i=1}^{n-1}R_i$\\~
Define Reachability set of $T$ for P0, $\Reach(T,0) := \bigcup_{i=1}^{n-1}R_i$\\~
A vertex $v\in R_i$: \\~
@ -184,7 +183,7 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\end{adjustbox}
\column{.5\textwidth} % Right column and width
\textbf{Definition} A type of vertex $x$ is a tuple $(y_1, \ldots, y_k)$, where each $x_i \in \{0,1\}$, such that $y_i=1$ iff $x$ is in $Reach (T_i, 0)$.
\textbf{Definition} A type of vertex $x$ is a tuple $(y_1, \ldots, y_k)$, where each $x_i \in \{0,1\}$, such that $y_i=1$ iff $x$ is in $\Reach (T_i, 0)$.
\end{columns}
\end{frame}
%frame 11
@ -204,8 +203,9 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
The minimum base of $T$ is the minimum subset of $T$ which can generate the same Reachability set as $T$.\\~
Computing the minimum base is NP-hard.\\~
Set cover problem: Given a set $S$ of n elements, a collections $S_1,S_2,...,S_m$ of subsets of $S$, and a number K, does there exists a collection of at most k of these sets whose union is equal to all of $S$.
\begin{problem}[Set cover]
Given a set $S$ of n elements, a collections $S_1,S_2,...,S_m$ of subsets of $S$, and a number K, does there exists a collection of at most k of these sets whose union is equal to all of $S$.
\end{problem}
\end{frame}
%frame 13
@ -250,10 +250,12 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\section{Büchi Game}
%frame 14
\begin{frame}{Büchi Game}
\textbf{Definition} A \textbf{Büchi game} is a game $\mathcal{G}=(G,s,T)$ where $G$ is the Reachability game graph, $V_i$ is an initial vertex, $T\subseteq V$ is the target set as in Reachability game.\\~
Play: The definition of play in Büchi Game is the same as in Reachability game.\\~
Definition of winning: We assume the play $P$ is infinite here.
if there exists infinite many vertices $v\in T$ in $P$, P0 wins. Otherwise P1 wins.
\begin{definition}[Büchi Game]
A \textbf{Büchi game} is a game $\mathcal{G}=(G,s,T)$ where $G$ is the Reachability game graph, $V_i$ is an initial vertex, $T\subseteq V$ is the target set as in Reachability game.\\~
Play: The definition of play in Büchi Game is the same as in Reachability game.\\~
Definition of winning: We assume the play $P$ is infinite here.
if there exists infinite many vertices $v\in T$ in $P$, P0 wins. Otherwise P1 wins.
\end{definition}
\end{frame}
%frame 15
@ -299,15 +301,15 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\draw[thick,fill=lightblue, fill opacity=0.3] (2,-2) -- (2,2) -- (6,2) -- (6,-2) -- cycle; % reach
\node[shape=circle,draw opacity=0](txt) at (3.5,-2.3) {$G$};
\node[shape=circle,draw opacity=0](txt) at (1,-1.7) {$T$};
\node[shape=circle,draw opacity=0](txt) at (4,1.7) {$Reach(T,0)$};
\node[shape=circle,draw opacity=0](txt) at (4,1.7) {$\Reach(T,0)$};
\end{tikzpicture}
\end{adjustbox}
\column{.35\textwidth} % Right column and width
If $v\notin Reach(T,0)\cup T$, $v$ can not reach $T$, P0 will lose.\\~
If $v\notin \Reach(T,0)\cup T$, $v$ can not reach $T$, P0 will lose.\\~
Some vertices in $T$ can not reach $Reach(T,0)\cup T$, P0 will also lose on these vertices.
Some vertices in $T$ can not reach $\Reach(T,0)\cup T$, P0 will also lose on these vertices.
\end{columns}
\end{frame}
@ -323,19 +325,19 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\node[shape=circle,draw opacity=0](txt) at (3.5,-2.3) {$G$};
\node[shape=circle,draw opacity=0](txt) at (1,-1.7) {$T_2$};
\node[shape=circle,draw opacity=0](txt) at (1,1.7) {$T_1$};
\node[shape=circle,draw opacity=0](txt) at (4,-1.7) {$Reach(T_2,0)$};
\node[shape=circle,draw opacity=0](txt) at (4,1.7) {$Reach(T,0)\backslash Reach(T_2,0)$};
\node[shape=circle,draw opacity=0](txt) at (4,-1.7) {$\Reach(T_2,0)$};
\node[shape=circle,draw opacity=0](txt) at (4,1.7) {$\Reach(T,0)\backslash \Reach(T_2,0)$};
\end{tikzpicture}
\end{adjustbox}
\column{.37\textwidth} % Right column and width
$T_1=\{v\in T|v$ can't reach $T\cup Reach(T,0)\}$\\~
$T_1=\{v\in T|v$ can't reach $T\cup \Reach(T,0)\}$\\~
Some vertices in $T_2$ can only reach $Reach(T,0)\backslash Reach(T_2,0)$\\~
Some vertices in $T_2$ can only reach $\Reach(T,0)\backslash \Reach(T_2,0)$\\~
We find $T_3=\{v\in T_2|v$ can't reach $T_2\cup Reach(T_2,0)\}$
We find $T_3=\{v\in T_2|v$ can't reach $T_2\cup \Reach(T_2,0)\}$
\end{columns}
\end{frame}
\begin{frame}{Algorithm for Büchi Game 1}
@ -352,7 +354,7 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\draw[thick,fill=red, fill opacity=0.3] (0,0.125) -- (0,0.25) -- (6,0.25) -- (6,0.125) -- cycle;
\node[shape=circle,draw opacity=0](txt) at (3.5,-2.3) {$G$};
\node[shape=circle,draw opacity=0](txt) at (1,1.7) {$T_1$};
\node[shape=circle,draw opacity=0](txt) at (4,1.7) {$Reach(T,0)\backslash Reach(T_2,0)$};
\node[shape=circle,draw opacity=0](txt) at (4,1.7) {$\Reach(T,0)\backslash \Reach(T_2,0)$};
\node[shape=circle,draw opacity=0](txt) at (2.1,-1.5) {Winning set for P0};
\end{tikzpicture}
@ -361,17 +363,17 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\column{.35\textwidth} % Right column and width
We repeat this process until $T_k$ does not shrink.\\~
The remaining part of $T_k\cup Reach(T_k,0)$ is the winning set for P0.
The remaining part of $T_k\cup \Reach(T_k,0)$ is the winning set for P0.
\end{columns}
\end{frame}
\begin{frame}{Algorithm for Büchi Game 1}
\begin{itemize}
\item How to find $T_1$\\
$T_1=\{v\in T|v$ can't reach $T\cup Reach(T,0)\}$\\
$T_1=\{v\in T|v$ can only reach $V\backslash \{T\cup Reach(T,0)\}\}$\\
P1 wants to reach $V\backslash \{T\cup Reach(T,0)\}\}$, P0 tries to avoid $V\backslash \{T\cup Reach(T,0)\}\}$.\\
compute $Reach(V\backslash \{T\cup Reach(T,0)\}\},1)$
$T_1=\{v\in T|v$ can't reach $T\cup \Reach(T,0)\}$\\
$T_1=\{v\in T|v$ can only reach $V\backslash \{T\cup \Reach(T,0)\}\}$\\
P1 wants to reach $V\backslash \{T\cup \Reach(T,0)\}\}$, P0 tries to avoid $V\backslash \{T\cup \Reach(T,0)\}\}$.\\
compute $\Reach(V\backslash \{T\cup \Reach(T,0)\}\},1)$
\item Time complexity\\
$O(m)$ to find $T_i$, at most $O(n)$ times. Worst-case $O(nm)$.
@ -390,7 +392,7 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\node[shape=circle,draw opacity=0](txt) at (3.5,-2.3) {$G$};
\node[shape=circle,draw opacity=0](txt) at (1,1.7) {$T$};
\node[shape=circle,draw opacity=0](txt) at (6.5,0) {$C_0\cup C_1$};
\node[shape=circle,draw opacity=0](txt) at (2,-1.7) {$Reach(C_0\cup C_1,1)$};
\node[shape=circle,draw opacity=0](txt) at (2,-1.7) {$\Reach(C_0\cup C_1,1)$};
\end{tikzpicture}
\end{adjustbox}
@ -402,7 +404,7 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
$C_0$ is a set of vertices in $V_0\backslash T$ having all outgoing edges to vertices in $V\backslash T$.\\
$C_1$ is a set of vertices in $V_1\backslash T$ having an outgoing edge to vertices in $V\backslash T$.\\~
Compute $Reach(C_0\cup C_1,1)$
Compute $\Reach(C_0\cup C_1,1)$
\end{columns}
\end{frame}
\begin{frame}{Algorithm for Büchi Game 2}
@ -421,21 +423,21 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\node[shape=circle,draw opacity=0](txt) at (6.5,0) {$C_0\cup C_1$};
\node[shape=circle,draw opacity=0](txt) at (1,-1.7) {$T_1$};
\node[shape=circle,draw opacity=0](txt) at (2.5,-1.7) {$D$};
\node[shape=circle,draw opacity=0](txt) at (5,-1.7) {$Reach(T_1\cup D,0)$};
\node[shape=circle,draw opacity=0](txt) at (5,-1.7) {$\Reach(T_1\cup D,0)$};
\node[shape=circle,draw opacity=0](txt) at (4,-0.75) {$E$};
\end{tikzpicture}
\end{adjustbox}
\column{.39\textwidth} % Right column and width
Some vertices in $Reach(C_0\cup C_1,1)$ can "reach" $T_1$.($D$ in the left picture)\\~
Some vertices in $\Reach(C_0\cup C_1,1)$ can "reach" $T_1$.($D$ in the left picture)\\~
Compute $Reach(T_1\cup D,0)$.\\~
Compute $\Reach(T_1\cup D,0)$.\\~
$E=Reach(C_0\cup C_1,1)\backslash \{T_1\cup D \cup Reach(T_1\cup D,0)\}$\\~
$E=\Reach(C_0\cup C_1,1)\backslash \{T_1\cup D \cup \Reach(T_1\cup D,0)\}$\\~
$\{E\cup C_0\cup C_1\}\backslash Reach(T_1\cup D,0)$ is the set of vertices which can't "reach" $T$.
$\{E\cup C_0\cup C_1\}\backslash \Reach(T_1\cup D,0)$ is the set of vertices which can't "reach" $T$.
\end{columns}
\end{frame}
\begin{frame}{Algorithm for Büchi Game 2}
@ -454,18 +456,18 @@ Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~
\node[shape=circle,draw opacity=0](txt) at (6.5,0) {$C_0\cup C_1$};
\node[shape=circle,draw opacity=0](txt) at (1,-1.7) {$T_1$};
\node[shape=circle,draw opacity=0](txt) at (2.5,-1.7) {$D$};
\node[shape=circle,draw opacity=0](txt) at (5,-1.7) {$Reach(T_1\cup D,0)$};
\node[shape=circle,draw opacity=0](txt) at (5,-1.7) {$\Reach(T_1\cup D,0)$};
\node[shape=circle,draw opacity=0](txt) at (4,-0.75) {$E$};
\end{tikzpicture}
\end{adjustbox}
\column{.4\textwidth} % Right column and width
$S=\{E\cup C_0\cup C_1\}\backslash Reach(T_1\cup D,0)$ is the same as $V\backslash \{T\cup Reach(T)\}$ in Algorithm 1.\\~
$S=\{E\cup C_0\cup C_1\}\backslash \Reach(T_1\cup D,0)$ is the same as $V\backslash \{T\cup \Reach(T)\}$ in Algorithm 1.\\~
Then we can compute $Reach(S,1)$ to delete some losing vertices for P0 in $T$.\\~
Then we can compute $\Reach(S,1)$ to delete some losing vertices for P0 in $T$.\\~
Repeat the same process on $G\backslash\{T\backslash Reach(S,1)\}$
Repeat the same process on $G\backslash\{T\backslash \Reach(S,1)\}$
\end{columns}
\end{frame}
\begin{frame}{Algorithm for Büchi Game 2}

Binary file not shown.

View File

@ -1,16 +1,4 @@
\documentclass{beamer}
\usepackage[english]{babel}
\usepackage{fancyhdr} % header footer
\usepackage{graphicx} % figure
\usepackage{booktabs}
\usepackage{xcolor}
\usepackage{bookmark}
\usepackage{hyperref}
\usepackage{graphicx} % Allows including images
\usepackage{booktabs} % Allows the use of \toprule, \midrule and \bottomrule in tables
\usepackage{tikz}
\usepackage[ruled,linesnumbered]{algorithm2e}
\usepackage{adjustbox}
\author{Yu Cong}
\title{Reachability and Büchi games}
@ -23,6 +11,7 @@
\usetheme{Simple}
% \useoutertheme{tree}
\DeclareMathOperator{\Reach}{Reach}
\begin{document}
\begin{frame}[plain]
@ -34,5 +23,5 @@
% Throughout your presentation, if you choose to use \section{} and \subsection{} commands, these will automatically be printed on this slide as an overview of your presentation
\tableofcontents
\end{frame}
\input{content.tex}
\input{Büchi Game-content.tex}
\end{document}

View File

@ -2,6 +2,44 @@
%
% This file may be distributed and/or modified
% under the LaTeX Project Public License
\RequirePackage[english]{babel}
\RequirePackage{fancyhdr} % header footer
\RequirePackage{xcolor}
\RequirePackage{bookmark}
\RequirePackage{hyperref}[colorlinks=true,urlcolor=Blue,citecolor=Green,linkcolor=BrickRed,unicode]
\RequirePackage{graphicx} % Allows including images
\RequirePackage{booktabs} % Allows the use of \toprule, \midrule and \bottomrule in tables
\RequirePackage{tikz}
\usetikzlibrary{backgrounds}
\usetikzlibrary{arrows,shapes}
\usetikzlibrary{tikzmark} % for \tikzmarknode
\usetikzlibrary{calc} % for computing the midpoint between two nodes, e.g. at ($(p1.north)!0.5!(p2.north)$)
\RequirePackage[ruled,linesnumbered]{algorithm2e}
\RequirePackage{adjustbox}
\RequirePackage{subcaption}
\RequirePackage{amsmath}
\RequirePackage{amsthm}
% a color box
\RequirePackage[breakable, theorems, skins]{tcolorbox}
\tcbset{enhanced}
\DeclareRobustCommand{\mybox}[2][gray!20]{%
\begin{tcolorbox}[ %% Adjust the following parameters at will.
breakable,
left=0pt,
right=0pt,
top=0pt,
bottom=0pt,
colback=#1,
colframe=#1,
width=\dimexpr\textwidth\relax,
enlarge left by=0mm,
boxsep=5pt,
arc=0pt,outer arc=0pt,
]
#2
\end{tcolorbox}
}
\definecolor{beamer@simple@color}{RGB}{12 72 66} % bluegreen
@ -14,6 +52,7 @@
\DeclareOptionBeamer{named}{\definecolor{beamer@simple@color}{named}{#1}}
\DeclareOptionBeamer{hsb}{\definecolor{beamer@simple@color}{hsb}{#1}}
\ProcessOptionsBeamer
\definecolor{oliver}{rgb}{0.33, 0.42, 0.18}
% footline
% delete navigation below
@ -101,7 +140,7 @@
\setbeamercolor{alerted text}{fg=beamer@simple@color}
\setbeamerfont{block title alerted}{series=\mdseries}
\setbeamerfont{alerted text}{series=\bfseries\boldmath}
\hypersetup{colorlinks,linkcolor=,urlcolor=beamer@simple@color!80!white}
\hypersetup{colorlinks,linkcolor=,urlcolor=oliver}
\usefonttheme[onlymath]{serif}
\setbeamerfont{frametitle}{series=\bfseries\boldmath}
\setbeamerfont{block title}{series=\bfseries\boldmath}
@ -122,6 +161,110 @@
\setbeamercolor{block title}{bg=mygrey!25!white}
\setbeamercolor{block body}{fg=black,bg=mygrey!13!white}
% more theorem env
\newtheorem{observation}{Observation}
\newtheorem{question}{Question}
% ----------------------------------------------------------------------
% Simple math stuff
% ----------------------------------------------------------------------
\renewcommand{\subset}{\subseteq}
% ---- SYMBOLS ----
\let\e\varepsilon % a ``real'' epsilon — better yet, just use Unicode ε.
%
% I give up. These are in the wrong font, but my kludged versions
% LOOK like kludges, especially \Z, \Q, and \C.
%
\def\Real{\mathbb{R}}
\def\Proj{\mathbb{P}}
\def\Hyper{\mathbb{H}}
\def\Integer{\mathbb{Z}}
\def\Natural{\mathbb{N}}
\def\Complex{\mathbb{C}}
\def\Rational{\mathbb{Q}}
\let\N\Natural
\let\Q\Rational
\let\R\Real
\let\Z\Integer
\def\Rd{\Real^d}
\def\RP{\Real\Proj}
\def\CP{\Complex\Proj}
% ---- OPERATORS (requires amsmath) ----
\def\aff{\operatorname{aff}}
\def\area{\operatorname{area}}
\def\argmax{\operatornamewithlimits{arg\,max}}
\def\argmin{\operatornamewithlimits{arg\,min}}
\def\Aut{\operatorname{Aut}} % Automorphism group
\def\card{\operatorname{card}} % cardinality, deprecated for \abs
\def\conv{\operatorname{conv}}
\def\E{\operatorname{E}} % Expectation: $\E[X]$ (like \Pr)
\def\EE{\operatornamewithlimits{E}}
\def\Hom{\operatorname{Hom}} % Homomorphism group
\def\id{\operatorname{id}} % identity
\def\im{\operatorname{im}} % image
\def\lcm{\operatorname{lcm}}
\def\lfs{\operatorname{lfs}} % local feature size
\def\poly{\operatorname{poly}}
\def\polylog{\operatorname{polylog}}
\def\rank{\operatorname{rank}}
\def\rel{\operatorname{rel\,}} % relative (interior, boundary, etc.)
\def\sgn{\operatorname{sgn}}
\def\vol{\operatorname{vol}} % volume
\def\fp#1{^{\underline{#1}}} % falling powers: $n\fp{d}$
\def\rp#1{^{\overline{#1}}} % rising powers: $n\rp{d}$
\def\setsymdiff{\operatorname{\triangle}}
% % --- Darts and fences ---
% % less nice replacements for stmaryrd characters
% \@ifundefined{shortrightarrow}{\let\shortrightarrow\rightarrow}{}
% \@ifundefined{shortleftarrow}{\let\shortleftarrow\leftarrow}{}
% \@ifundefined{shortuparrow}{\let\shortuparrow\uparrow}{}
% \@ifundefined{shortdownarrow}{\let\shortdownarrow\downarrow}{}
\def\arcto{\mathord\shortrightarrow}
\def\arcfrom{\mathord\shortleftarrow}
\def\arc#1#2{#1\arcto#2}
\def\cra#1#2{#1\mathord\shortleftarrow#2}
\def\fence#1#2{#1\mathord\shortuparrow#2}
\def\ecnef#1#2{#1\mathord\shortdownarrow#2}
% --- Cheap displaystyle operators ---
\def\Frac#1#2{{\displaystyle\frac{#1}{#2}}}
\def\Sum{\sum\limits}
\def\Prod{\prod\limits}
\def\Union{\bigcup\limits}
\def\Inter{\bigcap\limits}
\def\Lor{\bigvee\limits}
\def\Land{\bigwedge\limits}
\def\Lim{\lim\limits}
\def\Max{\max\limits}
\def\Min{\min\limits}
% ---- RELATORS ----
\def\deq{\stackrel{\scriptscriptstyle\triangle}{=}} % Use := instead.
\def\into{\DOTSB\hookrightarrow} % = one-to-one
\def\onto{\DOTSB\twoheadrightarrow}
\def\inonto{\DOTSB\lhook\joinrel\twoheadrightarrow}
\def\from{\leftarrow}
\def\tofrom{\leftrightarrow}
\def\mapsfrom{\mathrel{\reflectbox{$\mapsto$}}}
\def\longmapsfrom{\mathrel{\reflectbox{$\longmapsto$}}}
% ---- DELIMITER PAIRS ----
% --- always self-scaling delmiter pairs ---
\def\set#1{\left\{ #1 \right\}}
\def\floor#1{\left\lfloor #1 \right\rfloor}
\def\ceil#1{\left\lceil #1 \right\rceil}
\def\seq#1{\left\langle #1 \right\rangle}
\def\abs#1{\left| #1 \right|}
\def\norm#1{\left\| #1 \right\|}
\def\paren#1{\left( #1 \right)} % need better macro name!
\def\brack#1{\left[ #1 \right]} % need better macro name!
\def\indic#1{\left[ #1 \right]} % indicator variable; Iverson notation