diff --git a/content.tex b/Büchi Game-content.tex similarity index 87% rename from content.tex rename to Büchi Game-content.tex index 2283541..69c7e8b 100644 --- a/content.tex +++ b/Büchi Game-content.tex @@ -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} diff --git a/simple.pdf b/Büchi Games.pdf similarity index 58% rename from simple.pdf rename to Büchi Games.pdf index edfc765..b1934e2 100644 Binary files a/simple.pdf and b/Büchi Games.pdf differ diff --git a/simple.tex b/Büchi Games.tex similarity index 59% rename from simple.tex rename to Büchi Games.tex index abd10f7..c337cc3 100644 --- a/simple.tex +++ b/Büchi Games.tex @@ -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} \ No newline at end of file diff --git a/beamerthemeSimple.sty b/beamerthemeSimple.sty index 0506b83..672764b 100644 --- a/beamerthemeSimple.sty +++ b/beamerthemeSimple.sty @@ -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 +