<commit_before>\documentclass{beamer}

\usepackage[utf8]{inputenc}
\usepackage[absolute,overlay]{textpos}

\title{Model Checking World Domination}
\author{<NAME> \& <NAME>}
\institute{McGill University}
\date{29 March 2017}

%%%%% PACKAGES

\usepackage{tikz}
\usepackage{textcomp}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{listings}
\usepackage{graphicx}

%%%%% TIKZ

\usetikzlibrary{arrows,shapes,calc,graphs}

\tikzstyle{every picture}+=[remember picture]
\tikzset{
    ampersand replacement=\&,
    >=stealth',
    shorten >=1pt,
}

%%%%% THEOREMS

\theoremstyle{definition}
\newtheorem{defn}{Definition}

%%%%% LISTINGS

\lstset{basicstyle=\footnotesize\ttfamily}

%%%%% FONTS

\everymath{\displaystyle}
\usefonttheme{serif}

\setbeamercolor{framesource}{fg=gray}
\setbeamerfont{framesource}{size=\tiny}

%%%%% THEME

\usetheme{metropolis}

%%%%% COMMANDS 

\newcommand{\source}[1]{\begin{textblock*}{8cm}(0.5cm,8.6cm)
    \begin{beamercolorbox}[ht=0.5cm,left]{framesource}
        \usebeamerfont{framesource}\usebeamercolor[fg]{framesource} Source: {#1}
    \end{beamercolorbox}
\end{textblock*}}

\begin{document}

\frame{\titlepage}

\begin{frame}
    \frametitle{Robot apocalypse}

    \includegraphics[width=\textwidth]{nanobots.png}

    \pause

    \begin{itemize}
        \item
            If you're going to take over the world, \alert{do it right.}
    \end{itemize}
\end{frame}

\begin{frame}
    \frametitle{Philosophy of Swarm Robotics}
    \begin{itemize}
        \item
    "Achieve some desired, complex behavior using a collection of simple, individual agents."
    \end{itemize}
\end{frame}

% How swarm robotics and formal verification are connected
\begin{frame}
    \frametitle{Swarm Robotics - Formal Verification}

    \begin{itemize}
        \item Verification of swarm behavior (based on knowledge of individual design)
        \item \textbf{Optimization of swarm behavior}
    \end{itemize}
\end{frame}

% The results of real world actions are often uncertain. This motivates
% the usage of a probabilistic model to represent battles.
% We opt for the usage of discrete time Markov chains for simplicity
% and ease of construction. Our proposed model can be extended to
% continuous-time if necessary.
\begin{frame}
    \frametitle{DTMCs}
    \begin{defn}
        A \emph{discrete-time Markov Chain} (DTMC)
        is a tuple: $$ \mathcal{M} = (S, \mathbf{P}, \mathcal{d}_{init}, AP, L) $$
        \begin{itemize}
            \item $ S $ is the set of states,
            \item $ \mathbf{P} : S \times S \to [0, 1] $ is the transition probability function (matrix),
            \item $ \mathcal{d}_{init} : S \to [0, 1] $ is the initial distribution over states,
            \item AP, L as seen in class.
        \end{itemize}
    \end{defn}
\end{frame}

% Simple example of a DTMC.
% The point is to talk about probabilistic
% properties, like expectation.
\begin{frame}
    \frametitle{Example DTMC}
    \begin{center}
        \begin{tikzpicture}
            \matrix[row sep=3cm, column sep=3cm]{
                \node[draw=black,circle] (A) {A} ; \&
                \node[draw=black,circle] (B) {B} ; \\
            } ;

            \graph[use existing nodes] {
                A ->[edge label={$a[p]$},loop below]
                A ->[edge label={$a[1-p]$},bend left=70]
                B ;
            } ;
        \end{tikzpicture}
    \end{center}
\end{frame}

\begin{frame}
    \frametitle{Property Specification in PCTL}

    \begin{itemize}<commit_msg>remove mathcals that don't render properly<commit_after>\documentclass{beamer}

\usepackage[utf8]{inputenc}
\usepackage[absolute,overlay]{textpos}

\title{Model Checking World Domination}
\author{<NAME> \& <NAME>}
\institute{McGill University}
\date{29 March 2017}

%%%%% PACKAGES

\usepackage{tikz}
\usepackage{textcomp}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{listings}
\usepackage{graphicx}

%%%%% TIKZ

\usetikzlibrary{arrows,shapes,calc,graphs}

\tikzstyle{every picture}+=[remember picture]
\tikzset{
    ampersand replacement=\&,
    >=stealth',
    shorten >=1pt,
}

%%%%% THEOREMS

\theoremstyle{definition}
\newtheorem{defn}{Definition}

%%%%% LISTINGS

\lstset{basicstyle=\footnotesize\ttfamily}

%%%%% FONTS

\everymath{\displaystyle}
\usefonttheme{serif}

\setbeamercolor{framesource}{fg=gray}
\setbeamerfont{framesource}{size=\tiny}

%%%%% THEME

\usetheme{metropolis}

%%%%% COMMANDS 

\newcommand{\source}[1]{\begin{textblock*}{8cm}(0.5cm,8.6cm)
    \begin{beamercolorbox}[ht=0.5cm,left]{framesource}
        \usebeamerfont{framesource}\usebeamercolor[fg]{framesource} Source: {#1}
    \end{beamercolorbox}
\end{textblock*}}

\begin{document}

\frame{\titlepage}

\begin{frame}
    \frametitle{Robot apocalypse}

    \includegraphics[width=\textwidth]{nanobots.png}

    \pause

    \begin{itemize}
        \item
            If you're going to take over the world, \alert{do it right.}
    \end{itemize}
\end{frame}

\begin{frame}
    \frametitle{Philosophy of Swarm Robotics}
    \begin{itemize}
        \item
    "Achieve some desired, complex behavior using a collection of simple, individual agents."
    \end{itemize}
\end{frame}

% How swarm robotics and formal verification are connected
\begin{frame}
    \frametitle{Swarm Robotics - Formal Verification}

    \begin{itemize}
        \item Verification of swarm behavior (based on knowledge of individual design)
        \item \textbf{Optimization of swarm behavior}
    \end{itemize}
\end{frame}

% The results of real world actions are often uncertain. This motivates
% the usage of a probabilistic model to represent battles.
% We opt for the usage of discrete time Markov chains for simplicity
% and ease of construction. Our proposed model can be extended to
% continuous-time if necessary.
\begin{frame}
    \frametitle{DTMCs}
    \begin{defn}
        A \emph{discrete-time Markov Chain} (DTMC)
        is a tuple: $$ \mathcal{M} = (S, \mathbf{P}, d_{init}, AP, L) $$
        \begin{itemize}
            \item $ S $ is the set of states,
            \item $ \mathbf{P} : S \times S \to [0, 1] $ is the transition probability function (matrix),
            \item $ d_{init} : S \to [0, 1] $ is the initial distribution over states,
            \item AP, L as seen in class.
        \end{itemize}
    \end{defn}
\end{frame}

% Simple example of a DTMC.
% The point is to talk about probabilistic
% properties, like expectation.
\begin{frame}
    \frametitle{Example DTMC}
    \begin{center}
        \begin{tikzpicture}
            \matrix[row sep=3cm, column sep=3cm]{
                \node[draw=black,circle] (A) {A} ; \&
                \node[draw=black,circle] (B) {B} ; \\
            } ;

            \graph[use existing nodes] {
                A ->[edge label={$a[p]$},loop below]
                A ->[edge label={$a[1-p]$},bend left=70]
                B ;
            } ;
        \end{tikzpicture}
    \end{center}
\end{frame}

\begin{frame}
    \frametitle{Property Specification in PCTL}

    \begin{itemize}
{'fraction_non_alphanumeric': 0.13640908441651192, 'fraction_numerical': 0.007427510355663477, 'mean_word_length': 3.0995316159250588, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7625742', 'n_tokens_mistral': 2398, 'n_tokens_neox': 2307, 'n_words': 572}