From 006592fb09846d89de384d61a7611354a07ab722 Mon Sep 17 00:00:00 2001 From: congyu711 Date: Sun, 14 Jan 2024 16:26:48 +0800 Subject: [PATCH] change .sty --- bar169.tex | 32 +- beamerthemeBar169.sty | 34 ++- beamerthemeSimple.sty | 62 +++- content.tex | 686 +++++++++++++++++++++++++++++------------- simple.tex | 33 +- 5 files changed, 591 insertions(+), 256 deletions(-) diff --git a/bar169.tex b/bar169.tex index d9236aa..a207eeb 100644 --- a/bar169.tex +++ b/bar169.tex @@ -1,8 +1,28 @@ \documentclass[aspectratio=169]{beamer} - \input{pkgs.tex} - \input{global.tex} - \usetheme{Bar169} +\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} - \begin{document} - \input{content.tex} - \end{document} \ No newline at end of file +\author{Yu Cong} +\title{Reachability and Büchi games} +\date{\today} + +% \AtBeginSection[]{ +% \frame{\frametitle{Outline}\tableofcontents[currentsection, +% subsectionstyle=show/show/shaded]} +% } + +\usetheme{Bar169} + +\begin{document} + \input{content.tex} +\end{document} \ No newline at end of file diff --git a/beamerthemeBar169.sty b/beamerthemeBar169.sty index 5d94b17..c354380 100644 --- a/beamerthemeBar169.sty +++ b/beamerthemeBar169.sty @@ -17,7 +17,7 @@ % sidebar % on the right -\useoutertheme[width=5\baselineskip,right]{sidebar} +\useoutertheme[width=5\baselineskip,right,hideothersubsections]{sidebar} % delete title and author % \makeatletter \setbeamertemplate{sidebar right}{\insertverticalnavigation{\beamer@sidebarwidth}} @@ -27,7 +27,7 @@ \setbeamerfont{subsection in sidebar}{size=\scriptsize} % margin \setbeamersize{sidebar width right=3cm} -\setbeamersize{sidebar width left=2cm} +\setbeamersize{sidebar width left=0.5cm} @@ -38,23 +38,27 @@ % \makeatother \setbeamertemplate{footline} { - \leavevmode% - \hbox{% - \begin{beamercolorbox}[wd=.4\paperwidth,ht=2.25ex,dp=1ex,center]{author in head/foot}% - \usebeamerfont{author in head/foot}\insertshortauthor + \leavevmode% + \hbox{% + \begin{beamercolorbox}[wd=.2\paperwidth,ht=2.25ex,dp=1ex,center]{author in head/foot}% + \usebeamerfont{author in head/foot}\insertshortauthor \end{beamercolorbox} - - \begin{beamercolorbox}[wd=.6\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}% - \usebeamerfont{title in head/foot}\insertshorttitle\hspace*{13em} - \insertframenumber{} / \inserttotalframenumber\hspace*{0ex} - \end{beamercolorbox}} - - \vskip0pt% + + \begin{beamercolorbox}[wd=.7\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}% + \usebeamerfont{title in head/foot}\insertshorttitle + \end{beamercolorbox} + + \begin{beamercolorbox}[wd=.1\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}% + \usebeamerfont{title in head/foot}\insertframenumber{} / \inserttotalframenumber\hspace*{0ex} + \end{beamercolorbox} + } + + \vskip0pt% } % \makeatletter % footline color -\setbeamercolor{author in head/foot}{fg=black, bg=mygrey!5!white} -\setbeamercolor{title in head/foot}{fg=black, bg=mygrey!5!white} +\setbeamercolor{author in head/foot}{fg=black, bg=mygrey!10!white} +\setbeamercolor{title in head/foot}{fg=black, bg=mygrey!10!white} % item settings \setbeamertemplate{itemize item}{$\color{beamer@simple@color}\bullet$} diff --git a/beamerthemeSimple.sty b/beamerthemeSimple.sty index cc69d63..1215703 100644 --- a/beamerthemeSimple.sty +++ b/beamerthemeSimple.sty @@ -22,19 +22,59 @@ % \makeatother \setbeamertemplate{footline} { - \leavevmode% - \hbox{% - \begin{beamercolorbox}[wd=.4\paperwidth,ht=2.25ex,dp=1ex,center]{author in head/foot}% - \usebeamerfont{author in head/foot}\insertshortauthor + \leavevmode% + \hbox{% + \begin{beamercolorbox}[wd=.38\paperwidth,ht=2.25ex,dp=1ex,center]{author in head/foot}% + \usebeamerfont{author in head/foot}\insertshortauthor \end{beamercolorbox} - - \begin{beamercolorbox}[wd=.6\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}% - \usebeamerfont{title in head/foot}\insertshorttitle\hspace*{13em} - \insertframenumber{} / \inserttotalframenumber\hspace*{0ex} - \end{beamercolorbox}} - - \vskip0pt% + + \begin{beamercolorbox}[wd=.62\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}% + \usebeamerfont{title in head/foot}\insertshorttitle + \end{beamercolorbox} + + % \begin{beamercolorbox}[wd=.1\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}% + % \usebeamerfont{title in head/foot}\insertframenumber{} / \inserttotalframenumber\hspace*{0ex} + % \end{beamercolorbox} + } + + \vskip0pt% } +\useoutertheme{tree} +\makeatletter +\setbeamertemplate{headline} +{% + \begin{beamercolorbox}[wd=\paperwidth,colsep=1.5pt]{upper separation line head} + \end{beamercolorbox} + \begin{beamercolorbox}[wd=\paperwidth,ht=2.5ex,dp=1.125ex,% + leftskip=.3cm,rightskip=.3cm plus1fil]{title in head/foot} + \usebeamerfont{title in head/foot}\insertshorttitle + \usebeamerfont{section in head/foot}% + \ifbeamer@tree@showhooks + \setbox\beamer@tempbox=\hbox{\insertsectionhead}% + \ifdim\wd\beamer@tempbox>1pt% + \hskip2pt\raise1.9pt\hbox{\vrule width 5pt height0.4pt}% + \hskip1pt% + \fi% + \else% + \hskip6pt% + \fi% + \insertsectionhead + \usebeamerfont{subsection in head/foot}% + \ifbeamer@tree@showhooks + \setbox\beamer@tempbox=\hbox{\insertsubsectionhead}% + \ifdim\wd\beamer@tempbox>1pt% + \hskip2pt\raise1.9pt\hbox{\vrule width 5pt height0.4pt}% + \hskip1pt% + \fi% + \else% + \hskip12pt% + \fi% + \insertsubsectionhead\hfill\insertframenumber/\inserttotalframenumber\hspace{0.5em} + \end{beamercolorbox} + \begin{beamercolorbox}[wd=\paperwidth,colsep=1.5pt]{lower separation line head} + \end{beamercolorbox} +} +\makeatother % \makeatletter % footline color \setbeamercolor{author in head/foot}{fg=black, bg=mygrey!5!white} diff --git a/content.tex b/content.tex index 421cb63..c6ac6dc 100644 --- a/content.tex +++ b/content.tex @@ -1,236 +1,488 @@ -\frame[plain]{\titlepage} -\frame{\frametitle{Outline}\tableofcontents} +\definecolor{lightblue}{rgb}{0.67,0.87,0.9} -\section{Introduction} +\begin{frame}[plain] + % Print the title page as the first slide + \titlepage +\end{frame} -\begin{frame} - \frametitle{Latex and Beamer} - - LaTeX is a high-quality typesetting system; - it includes features designed for the production of - technical and scientific documentation. - - \vspace{0.4cm} - - \pause - - Beamer is a LaTeX class to create powerful, - flexible and nice-looking presentations and slides. - - The beamer class is focussed on producing (on-screen) presentations, - along with support material such as handouts and speaker notes. +\begin{frame}{Overview} + % 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} + +%------------------------------------------------ +\section{Motivation \& References} +%------------------------------------------------ +\begin{frame}{Motivation \& References} + Motivation: Reachability and Büchi games are important in system verification and testing. Computing the winning set of Büchi games is a central problem in computer aided verification with a large number of applications.\\~ + References: \\~ + \footnotesize{ + \begin{thebibliography}{99} + \bibitem[Smith, 2012]{p1} John Smith (2012) + \newblock Title of the publication + \newblock \emph{Journal Name} 12(3), 45 -- 678. + \end{thebibliography} + } \end{frame} - -\section{Beamer Basic} -\subsection{Hightlight} - -\begin{frame} - \frametitle{Block and Alert} - - \begin{block}{Pythagorean theorem} - \vspace*{-\baselineskip}\setlength\belowdisplayshortskip{0.6pt} - $$a^2 + b^2 = c^2$$ - % \vspace*{-\baselineskip}\setlength\belowdisplayshortskip{0.1pt} - where c represents the length of the hypotenuse and - a and b the lengths of the triangle's other two sides. - \end{block} - - \begin{alertblock}{Remark} - \begin{itemize} - \item the environment above is \alert{block} - \item the environment here is \alert{alertblock} - \end{itemize} - \end{alertblock} - +\section{Reachability Game} +\begin{frame}{Reachability Game} + A reachability game is a 2-player (namely P0 and P1) game on a directed finite graph.\\~ + Game graph: directed graph $G(\{V_0\cup V_1\},E)$.($\{V_0,V_1\}$is a partition of $V$) \\~ + Target set: target set is $T\subseteq \{V_0\cup V_1\}$.\\~ + A play $P$ is a (finite or infinite) path in the game graph beginning at the initial vertex $s$. If $v\in V_0$, P0 moves along an outgoing edge of v. Otherwise, P1 takes the move.\\~ + Definition of winning: P0 wins if $T\cap P \neq \emptyset$, otherwise P1 wins.\\~ + Memoryless strategy: a strategy for P0 is a mapping $\alpha : V_0 \rightarrow V$ that defines how P0 should extend the current play. \end{frame} +%frame 5 +\begin{frame}{Example for Reachability Game} +Rectangle vertices are in $V_1$, circles are in $V_0$;\\ +Vertices in $T$ are red, the initial vertex $v_I$ is blue.\\~ -\begin{frame} - \frametitle{Proof} - \begin{block}{Pythagorean theorem} - \vspace*{-\baselineskip}\setlength\belowdisplayshortskip{0.1pt} - $$a^2 + b^2 = c^2$$ - % \vspace*{-\baselineskip}\setlength\belowdisplayshortskip{0.2pt} - \end{block} - - \vspace{0.4cm} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment - \begin{proof} - \vspace*{-\baselineskip}\setlength\belowdisplayshortskip{0pt} - \begin{align*} - &3^2 + 4^2 = 5^2\\ - &5^2 + 12^2 = 13^2 - \end{align*} - % \vspace*{-\baselineskip}\setlength\belowdisplayshortskip{0pt} - \end{proof} -\end{frame} + \column{.45\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \node[shape=circle,draw=red] (1) at (0,0) {1}; + \node[shape=rectangle,draw=black] (2) at (0,4) {2}; + \node[shape=rectangle,draw=black] (3) at (2.5,4) {3}; + \node[shape=circle,draw=black] (4) at (5,0) {4}; + \node[shape=circle,draw=blue] (5) at (2.5,0) {5}; + \node[shape=rectangle,draw=black] (6) at (5,4) {6} ; + \path [->] (2) edge[thick] node[] {} (1); + \path [->] (2) edge[thick] node[] {} (4); + \path [->] (6) edge[thick,bend left=15] node[] {} (4); + \path [->] (4) edge[thick,bend left=15] node[] {} (6); + \path [->] (5) edge[thick,bend left=15] node[] {} (6); + \path [->] (6) edge[thick,bend right=15] node[] {} (1); + \path [->] (5) edge[thick] node[] {} (3); + \path [->] (3) edge[thick,bend right=20] node[] {} (1); + \end{tikzpicture} + \end{adjustbox} -\subsection{Other Environments} - -\begin{frame}{Algorithm} - \scriptsize - \begin{algorithm}[H] - \KwData{this text} - \KwResult{how to write algorithm with \LaTeX2e } - initialization\; - \While{not at end of this document}{ - read current\; - \eIf{understand}{ - go to next section\; - current section becomes this one\; - }{ - go back to the beginning of current section\; - } - } - \caption{How to write algorithms - (copied from \href{https://en.wikibooks.org/wiki/LaTeX/Algorithms}{here})} - \end{algorithm} -\end{frame} - -\begin{frame}[fragile] - \frametitle{An Algorithm For Finding Primes Numbers.} - \scriptsize - \begin{verbatim} - int main (void) - { - std::vector is_prime (100, true); - for (int i = 2; i < 100; i++) - if (is_prime[i]) - { - std::cout << i << " "; - for (int j = i; j < 100; is_prime [j] = false, j+=i); - } - return 0; - } - \end{verbatim} - - \vspace{-0.7cm} - - \begin{uncoverenv} - Note the use of \verb|\alert|. - \end{uncoverenv} -\end{frame} - -\begin{frame}{More} - More environments such as - - \begin{itemize} - \item Definition - \item lemma - \item corollary - \item example - \end{itemize} -\end{frame} - -\section{Beamer More} - -\subsection{Split Screen} - -\begin{frame}{Minipage} - \begin{minipage}{0.5\linewidth} - \begin{figure}[h] - \includegraphics[width=\textwidth]{imgs/pythagorean.jpg} - \end{figure} - \end{minipage}% - \hfill - \begin{minipage}{0.4\linewidth} - \begin{enumerate} - \item item - \item another - \item more - \begin{itemize} - \item first - \item second - \item third - \end{itemize} - \end{enumerate} - \end{minipage} -\end{frame} - -\begin{frame}{Columns} - \begin{columns} - \column{0.5\textwidth} - This is a text in first column. - $$E=mc^2$$ - \begin{itemize} - \item First item - \item Second item - \end{itemize} - - \column{0.5\textwidth} - \begin{block}{first block} - columns achieves splitting the screen - \end{block} - \begin{block}{second block} - stack block in columns - \end{block} - + \column{.5\textwidth} % Right column and width + A winning play for P0 is $\{5,3,1\}$\\~ \end{columns} \end{frame} -\subsection{Table} - -\begin{frame}{Create Tables} - \begin{center} - \begin{table}[!t] - % \caption{Three line} - % \label{table_time} - \begin{tabular}{ccc} - \toprule - first&second&third\\ - \midrule - 1 & 2 & 3 \\ - 4 & 5 & 6 \\ - 7 & 8 & 9 \\ - \bottomrule - \end{tabular} - \end{table} - \end{center} +%frame 6 +\begin{frame}{Algorithm for Reachability Game} +\begin{figure} + \centering + \begin{adjustbox}{width=0.3\textwidth} + \begin{tikzpicture} + % \draw (0,0) node {}; + \draw[fill=lightblue] (6,0) ellipse (28pt and 20pt); + \draw[] (7,0) ellipse (58pt and 40pt); + \node[shape=circle,draw=lightblue](t) at (6,0) {$T$}; + \node[shape=circle,draw=white](o) at (7,2.4) {}; + \node[shape=circle,draw=black] (1) at (7.8,0.5) {}; + \node[shape=rectangle,draw=black] (2) at (8.1,-0.5) {}; + \path [->] (1) edge[thick] node[] {} (t); + \path [->] (1) edge[thick] node[] {} (o); + \path [->] (2) edge[thick,bend left=15] node[] {} (t); + \path [->] (2) edge[thick,bend right=15] node[] {} (t); + \node[shape=circle,draw opacity=0](txt) at (7,-1) {Rank 1}; + \end{tikzpicture} + \end{adjustbox} +\end{figure} + \begin{itemize} + \item if $s$ is in $T$, P0 wins; + \item if $s\in V_0$ and $s$ has at least one outgoing edge to $u\in T$, P0 wins in one step; + \item if $s\in V_1$ and all of $s$'s outgoing edges go to $u\in T$, P0 wins in one step; + \end{itemize} \end{frame} - -\subsection{Math} - -\begin{frame}{Equation1} - A matrix in text must be set smaller: - $\bigl(\begin{smallmatrix} - a&b \\ c&d - \end{smallmatrix} \bigr)$ - to not increase leading in a portion of text. - - \[ f(n) = - \begin{cases} - n/2 & \quad \text{if } n \text{ is even}\\ - -(n+1)/2 & \quad \text{if } n \text{ is odd} - \end{cases} - \] - - $$50 apples \times 100 apples = lots of apples^2$$ -\end{frame} - -\begin{frame}{Equation2} - $$\sum_{\substack{04\right)$$ - - $$( a ), [ b ], \{ c \}, | d |, \| e \|, - \langle f \rangle, \lfloor g \rfloor, - \lceil h \rceil, \ulcorner i \urcorner$$ -\end{frame} - -\begin{frame}{Equation3} - $$Q(\alpha)=\alpha_i\alpha_jy_iy_j(x_i\cdot x_j)$$ - - $$Q(\alpha)=\alpha^i\alpha^jy^{(i)}y^{(j)}(x^i\cdot x^j)$$ +%frame 7 +\begin{frame}{Algorithm for Reachability Game} + We defined Rank 0 and Rank 1 already, now we define Rank i.\\ - $$\Gamma=\beta+\alpha+\gamma+\rho$$ + $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$\\~ + + + A vertex $v\in R_i$: \\~ + if $v \in V_0$ and there is an edge $e(v,u)\quad u\in R_{i-1}$;\\~ + if $v \in V_1$ and for every edge $e(v,u)$ we have $u\in \bigcup_{j=0}^{i-1} R_j$;\\ + +\end{frame} +%frame 8 +\begin{frame}{Algorithm for Reachability Game} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment + \column{.35\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \node[shape=circle,draw=red] (1) at (0,0) {1}; + \node[shape=circle,draw=red] (2) at (2,0) {2}; + \node[shape=circle,draw=blue] (3) at (4,0) {3}; + \node[shape=rectangle,draw=black] (4) at (0,3) {4}; + \node[shape=rectangle,draw=black] (5) at (2,3) {5}; + \node[shape=rectangle,draw=black] (6) at (4,3) {6} ; + \path [->] (3) edge[thick] node[] {} (6); + \path [->] (3) edge[thick] node[] {} (5); + \path [->] (5) edge[thick] node[] {} (1); + \path [->] (5) edge[thick] node[] {} (2); + \path [->] (4) edge[thick] node[] {} (1); + \path [->] (4) edge[thick] node[] {} (3); + \path [->] (6) edge[thick, bend right=30] node[] {} (4); + \end{tikzpicture} + \end{adjustbox} + + \column{.6\textwidth} % Right column and width + + \begin{itemize} + \item $R_0=\{1,2\}$; + \item $R_1=\{5\}$; + \item $R_2=\{3\}$; + \item $R_3=\{4\}$; + \item $R_4=\{6\}$; + \end{itemize} + For simplicity, denote $u\in R_k$ by Rank[$u$]=k. + \end{columns} +\end{frame} +% frame 9 +\begin{frame}{An O(m) Algorithm for Reachability Game} + \begin{algorithm}[H] + \scriptsize + \SetAlgoLined + \KwData{game graph $G$, target set $T$} + \KwResult{Rank[$|V|$]} + Q:= an empty queue\; + Rank[$|V|$],count[$|V|$]:= all 0s array\; + Q.push({T})\; + \While{Q is not empty}{ + $u$:=Q.front,Q.pop\; + \For{$e(v,u)\in E$}{ + \uIf{$v\in V_0$ and $v$ has not been visited} + {Rank[$v$]:=Rank[$u$]+1; Q.push($\{v\}$)} + \ElseIf{$v\in V_1$}{ + count[v]:=count[v]+1\; + \lIf{count[v]=Out Degree of $v$}{ + Rank[$v$]:=Rank[$u$]+1; Q.push($\{v\}$) + } + } + } + } + + \caption{Reachability for P0} + \end{algorithm} + Every edge is used at most once. +\end{frame} +%frame 10 +\begin{frame}{Type} + $T_1,T_2,...,T_k$ are disjoint subsets of $V$, now we want to compute Reachability of each one of them.\\~\\ + + + \begin{columns} + \column{.45\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw (0,0) node {}; + %\draw[fill=lightblue] (1,0) ellipse (28pt and 20pt); + \draw[] (2,1) ellipse (78pt and 60pt); + \node[shape=circle,draw=lightblue,fill =lightblue](t) at (1,0) {$T_1$}; + \node[shape=circle,draw=lightblue,fill =lightblue](t) at (2.2,0) {$T_2$}; + \node[shape=circle,draw=lightblue,fill =lightblue](t) at (3.4,0) {$T_3$}; + % \node[shape=circle,draw=white](o) at (2,2.4) {}; + %\node[shape=circle,draw=black] (1) at (2.8,0.5) {}; + % \node[shape=rectangle,draw=black] (2) at (3.1,-0.5) {}; + + \end{tikzpicture} + \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)$. + \end{columns} +\end{frame} +%frame 11 +\begin{frame}{Compute Types} + \begin{itemize} + \item Run reachability algorithm for every $T_i$, $O(km)$; + \item Compute simultaneously. +% \begin{itemize} +% \item similar to Algorithm 1, updating Ranks is replaced with updating Types. +% \item one update needs $O(k)$, $O(m)$ times of update is needed. $O(km)$ +% \end{itemize} + \item Can it be done in linear or nearly linear time? + \end{itemize} +\end{frame} +%frame 12 +\begin{frame}{Minimum Base} + 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$. + +\end{frame} +%frame 13 +\begin{frame}{Minimum Base} + \textbf{Proof}:\\ + We prove that the decision problem for minimum base is NP-Complete.\\ + The decision problem $L$ is can we find a base with at most k vertices.\\ + \begin{enumerate} + \item $L$ is in NP. + \item set cover problem(which is NP-Complete) can be reduced to $L$ in polynomial time. + \begin{itemize} + \item Construct a Reachability game graph $G(V_0,E)$. There are $m$ vertices in $T$ representing $m$ subsets in set cover problem, $n$ vertices not in $T$ representing $n$ elements in $S$. + \item If subset $S_i$ contains element $x_j$, connect an edge from vertex representing $S_i$ to vertex representing $x_j$ in $T$. + \end{itemize} + \end{enumerate} + %So $L$ is NP-Complete. The minimum base problem is NP-Hard. +\end{frame} +\begin{frame}{Minimum Base} + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw (0,0) node {}; + \node[shape=circle,draw=lightblue,fill =lightblue](t1) at (4,0) {$S_1$}; + \node[shape=circle,draw=lightblue,fill =lightblue](t2) at (5.2,0) {$S_2$}; + \node[shape=circle,draw=lightblue,fill =lightblue](t3) at (6.4,0) {$S_3$}; + \node[shape=circle,draw=black](x1) at (3,2) {$x_1$}; + \node[shape=circle,draw=black](x2) at (5,2) {$x_2$}; + \node[shape=circle,draw=black](x3) at (7,2) {$x_3$}; + \node[shape=circle,draw=black](x4) at (9,2) {$\ldots$}; + \path [->] (x1) edge[thick] node[] {} (t1); + \path [->] (x2) edge[thick] node[] {} (t1); + \path [->] (x1) edge[thick] node[] {} (t2); + \path [->] (x3) edge[thick] node[] {} (t2); + \end{tikzpicture} + \end{adjustbox}\\ + + $S_1=\{x_1,x_2\}$\\ + $S_2=\{x_1,x_3\}$\\~ + + So $L$ is NP-Complete. The minimum base problem is NP-Hard. \end{frame} +\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. + +\end{frame} +%frame 15 +\begin{frame}{Example for Büchi Game} + \begin{columns} + \column{0.45\textwidth} + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \node[shape=rectangle,draw=black] (1) at (0,0) {1}; + \node[shape=circle,draw=black] (2) at (1.5,0) {2}; + \node[shape=circle,draw=black] (3) at (4.5,0) {3}; + \node[shape=circle,draw=black] (4) at (0,3) {4}; + \node[shape=rectangle,draw=red] (5) at (1.5,3) {5}; + \node[shape=rectangle,draw=black] (6) at (3,3) {6} ; + \node[shape=rectangle,draw=red] (7) at (4.5,3) {7} ; + \path [->] (4) edge[thick] node[] {} (5); + \path [->] (5) edge[thick] node[] {} (6); + \path [->] (6) edge[thick] node[] {} (7); + \path [->] (3) edge[thick] node[] {} (7); + \path [->] (2) edge[thick] node[] {} (3); + \path [->] (1) edge[thick] node[] {} (2); + \path [->] (1) edge[thick] node[] {} (5); + \path [->] (5) edge[thick] node[] {} (2); + \path [->] (6) edge[thick] node[] {} (2); + \path [->] (7) edge[thick] node[] {} (2); + \path [->] (2) edge[thick,bend right=15] node[] {} (7); + + \end{tikzpicture} + \end{adjustbox} + \column{0.5\textwidth} + % P0 can force a visit from any vertex in $S=\{2,3,5,6,7\}$ to any other vertex in $S$.\\~ + + P0 is always winning on this game graph. + \end{columns} +\end{frame} +\begin{frame}{Algorithm for Büchi Game 1} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment + \column{.6\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw[thick, fill opacity=0.3] (0,-2) -- (0,2) -- (8,2) -- (8,-2) -- cycle; % G + \draw[thick,fill=blue, fill opacity=0.3] (0,-2) -- (0,2) -- (2,2) -- (2,-2) -- cycle; % T + \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)$}; + + \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.\\~ + + Some vertices in $T$ can not reach $Reach(T,0)\cup T$, P0 will also lose on these vertices. + + \end{columns} +\end{frame} +\begin{frame}{Algorithm for Büchi Game 1} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment + \column{.6\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw[thick, fill opacity=0.3] (0,-2) -- (0,2) -- (8,2) -- (8,-2) -- cycle; % G + \draw[thick,fill=blue, fill opacity=0.3] (0,-2) -- (0,2) -- (2,2) -- (2,-2) -- cycle; % T + \draw[thick,fill=lightblue, fill opacity=0.3] (2,-2) -- (2,2) -- (6,2) -- (6,-2) -- cycle; % reach + \draw[thick,fill=red, fill opacity=0.3] (0,1) -- (0,2) -- (6,2) -- (6,1) -- 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_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)$}; + + \end{tikzpicture} + \end{adjustbox} -\section{Conclusion} + \column{.37\textwidth} % Right column and width + $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)$\\~ + + 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} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment + \column{.6\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw[thick, fill opacity=0.3] (0,-2) -- (0,2) -- (8,2) -- (8,-2) -- cycle; % G + \draw[thick,fill=blue, fill opacity=0.3] (0,-2) -- (0,2) -- (2,2) -- (2,-2) -- cycle; % T + \draw[thick,fill=lightblue, fill opacity=0.3] (2,-2) -- (2,2) -- (6,2) -- (6,-2) -- cycle; % reach + \draw[thick,fill=red, fill opacity=0.3] (0,1) -- (0,2) -- (6,2) -- (6,1) -- cycle; + \draw[thick,fill=red, fill opacity=0.3] (0,0.5) -- (0,1) -- (6,1) -- (6,0.5) -- cycle; + \draw[thick,fill=red, fill opacity=0.3] (0,0.25) -- (0,0.5) -- (6,0.5) -- (6,0.25) -- cycle; + \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 (2.1,-1.5) {Winning set for P0}; -\begin{frame}{End} - The last page. -\end{frame} \ No newline at end of file + \end{tikzpicture} + \end{adjustbox} + + \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. + \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)$ + + \item Time complexity\\ + $O(m)$ to find $T_i$, at most $O(n)$ times. Worst-case $O(nm)$. + \end{itemize} +\end{frame} + +\begin{frame}{Algorithm for Büchi Game 2} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment + \column{.6\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw[thick, fill opacity=0.3] (0,-2) -- (0,2) -- (8,2) -- (8,-2) -- cycle; % G + \draw[thick,fill=blue, fill opacity=0.3] (0,-2) -- (0,2) -- (2,2) -- (2,-2) -- cycle; % T + \draw[thick,fill=lightblue, fill opacity=0.3] (2,-2) -- (2,2) -- (5,2) -- (5,-2) -- cycle; % reach + \draw[thick,fill=red, fill opacity=0.3] (0,-2) -- (0,-0.5) -- (5,-0.5) -- (5,-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 (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)$}; + + \end{tikzpicture} + \end{adjustbox} + + + \column{.35\textwidth} % Right column and width + Compute $C_0$ and $C_1$.\\~ + + $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)$ + \end{columns} +\end{frame} +\begin{frame}{Algorithm for Büchi Game 2} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment + \column{.6\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw[thick, fill opacity=0.3] (0,-2) -- (0,2) -- (8,2) -- (8,-2) -- cycle; % G + \draw[thick,fill=blue, fill opacity=0.3] (0,-2) -- (0,2) -- (2,2) -- (2,-2) -- cycle; % T + \draw[thick,fill=lightblue, fill opacity=0.3] (2,-2) -- (2,2) -- (5,2) -- (5,-2) -- cycle; % reach + \draw[thick,fill=red, fill opacity=0.3] (0,-2) -- (0,-0.5) -- (5,-0.5) -- (5,-2) -- cycle; % reach + \draw[thick,fill=red, fill opacity=0.3] (2,-2) -- (2,-0.5) -- (3,-0.5) -- (3,-2) -- cycle; % reach + \draw[thick,fill=purple, fill opacity=0.3] (3,-2) -- (3,-1) -- (8,-1) -- (8,-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 (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 (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)\\~ + + 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\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} + \begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment + \column{.6\textwidth} % Left column and width + \begin{adjustbox}{width=\textwidth} + \begin{tikzpicture} + \draw[thick, fill opacity=0.3] (0,-2) -- (0,2) -- (8,2) -- (8,-2) -- cycle; % G + \draw[thick,fill=blue, fill opacity=0.3] (0,-2) -- (0,2) -- (2,2) -- (2,-2) -- cycle; % T + \draw[thick,fill=lightblue, fill opacity=0.3] (2,-2) -- (2,2) -- (5,2) -- (5,-2) -- cycle; % reach + \draw[thick,fill=red, fill opacity=0.3] (0,-2) -- (0,-0.5) -- (5,-0.5) -- (5,-2) -- cycle; % reach + \draw[thick,fill=red, fill opacity=0.3] (2,-2) -- (2,-0.5) -- (3,-0.5) -- (3,-2) -- cycle; % reach + \draw[thick,fill=purple, fill opacity=0.3] (3,-2) -- (3,-1) -- (8,-1) -- (8,-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 (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 (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.\\~ + + 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)\}$ + \end{columns} +\end{frame} +\begin{frame}{Algorithm for Büchi Game 2} + \begin{itemize} + \item Time complexity\\~ + + Finding $S$ needs $O(m)$ time.\\ + Also in the worst case we need to compute $S$ $O(n)$ times. worst case $O(nm)$. + \end{itemize} +\end{frame} +%------------------------------------------------ diff --git a/simple.tex b/simple.tex index e754344..8ea6d1a 100644 --- a/simple.tex +++ b/simple.tex @@ -1,10 +1,29 @@ \documentclass{beamer} - \input{pkgs.tex} - \input{global.tex} +\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} +\date{\today} + +% \AtBeginSection[]{ +% \frame{\frametitle{Outline}\tableofcontents[currentsection, +% subsectionstyle=show/show/shaded]} +% } - \usetheme{Simple} - \useoutertheme{tree} +\usetheme{Simple} +% \useoutertheme{tree} - \begin{document} - \input{content.tex} - \end{document} \ No newline at end of file +\begin{document} + \input{content.tex} +\end{document} \ No newline at end of file