Commit c7291c06 authored by Quentin Aristote's avatar Quentin Aristote
Browse files

finish beamer

parent e158a790
\documentclass{beamer}
\usecolortheme{seahorse}
\setbeamertemplate{footline}[frame number]
% \setbeamertemplate{navigation symbols}{}
\setbeamertemplate{navigation symbols}{}
\usepackage{amsmath}
\usepackage{amssymb}
......@@ -17,6 +17,7 @@
\usepackage{tabularx}
\usepackage{fontspec}
\newfontfamily\DejaSans{DejaVu Sans}
\usepackage{appendixnumberbeamer}
\newcommand{\sem}[1]{\left\llbracket\,#1\,\right\rrbracket}
\newcommand{\clatfibration}{$\mathbf{CLat}_\sqcap$-fibration}
......@@ -57,21 +58,24 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{Cadre fibrationnel pour point fixes imbriqués \\ \& \\Notions de (bi)simulations pour automates de B\"uchi}
\author{Quentin Aristote}
\author{Quentin Aristote \\ \small supervisé par Ichiro Hasuo \& Jérémy Dubut}
\date{}
\maketitle
% Bonjour
% je vais présenter mon stage qui portait sur <titre>
% l'objectif de ce stage était de généraliser des résultats existants qui établissaient un lien entre théorie des jeux et \nu d'un opérateur fibrationnel : j'avais pour but d'établier un lien entre théorie des jeux, encore une fois, et points fixes imbriqués (et non plus seulement) plus grands points fixes
% ces résultats avaient été appliqués pour généraliser la notion de bisimulation ainsi que son lien avec la théorie des jeux
% l'espoir était donc de pouvoir faire de même avec les bisimulations pour automates de buchi, qui n'entraient pas dans ce cadre puisqu'elles s'expriment avec des points fixes imbriqués et non des plus grands points fixes
% Bonjour à tous
% je vais donc vous présenter le travail effectué durant mon stage qui portait sur <titre>
% l'objectif de ce stage était de généraliser des résultats existants qui établissaient un lien entre théorie des jeux et \nu d'un opérateur fibrationnel : la première partie de mon stage avait donc pour but d'établir un lien entre, encore une fois, la théorie des jeux, et, cette fois-ci, des points fixes imbriqués (et non plus seulement des plus grands points fixes)
% ces résultats préexistants avaient été appliqués pour généraliser la notion de bisimulation ainsi que son lien avec la théorie des jeux
% la seconde partie de mon stage avait donc pour but de faire de même avec les bisimulations pour automates de buchi, qui n'entraient pas dans le cadre existant puisqu'elles s'expriment avec des points fixes imbriqués et non pas des plus grands points fixes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Préliminaire : bisimulations}
\begin{center}
$x \sim y$ ssi le programme s'éxecute de la même façon depuis $x$ et $y$
\end{center}
\begin{figure}[h]
\centering
\begin{tikzpicture}
......@@ -129,8 +133,7 @@
\node (F) at (6,-1.5) {} ;
\end{scope}
}
\uncover<9->{
\uncover<11->{
\begin{scope}[every node/.style={left}]
\node at (0,-.5) {$\exists$} ;
\node at (3,-1.5) {$\forall$} ;
......@@ -142,12 +145,13 @@
}
\end{tikzpicture}
\end{figure}
\uncover<2-7>{
\[ c : X \rightarrow \mathcal{P}(X) \]
\uncover<2->{
\[ c : X \rightarrow \only<2-7>{\mathcal{P}}\only<8->{F}(X) \]
}
\uncover<8->{
\[ c : X \rightarrow FX \]
\uncover<9->{
\[ \varphi := \varphi_1 \wedge \varphi_2 \mid \varphi_1 \vee \varphi_2 \mid \uncover<10->{\exists\varphi \mid \forall\varphi} \]
}
\end{frame}
% bisimulation : relation d'équivalence sur états d'un programme qui relie les états depuis lesquels le programme a le meme comportement -> utile par exemple pour prouver le bon fonctionnement d'un compilateur
......@@ -265,9 +269,7 @@
}
\end{tikzpicture}
\end{figure}
\uncover<8->{
\[ \Phi_c^{\boldsymbol{\Omega},\tau} (\seq{P}{n}) = \bigsqcap_{\substack{f_1 : P_1 \drarrow \boldsymbol{\Omega} \\ \ldots \\ f_n : P_n \drarrow \boldsymbol{\Omega}}} (\tau \circ F\langle\seq{f}{n}\rangle \circ c)^*\boldsymbol{\Omega} \]
}
\[ \Phi_c^{\boldsymbol{\Omega},\tau} (\seq{P}{n}) = \bigsqcap_{\uncover<8->{\substack{f_1 : P_1 \drarrow \boldsymbol{\Omega} \\ \ldots \\ f_n : P_n \drarrow \boldsymbol{\Omega}}}} (\tau \circ F\langle\seq{f}{n}\rangle \circ c)^*\boldsymbol{\Omega} \]
\end{frame}
% d'abord opérateur fibrationnel = transformateur de prédicats
......@@ -299,7 +301,7 @@
\end{align*}
}
\uncover<4->{
Système d'équations à codensité :
Ici :
\begin{align*}
u_1 &=_{\eta_1} \Phi_{c_i}^{\boldsymbol{\Omega}_1,\tau_1}(\seq{u}{m}) \\
&\cdots \\
......@@ -325,7 +327,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Jeux de parité à codensité}
\frametitle{Lien avec la théorie des jeux}
\[ \Phi_{c_i}^{\boldsymbol{\Omega}_i,\tau_i} (\seq{P}{m}) = \bigsqcap_{\substack{f_1 : P_1 \drarrow \boldsymbol{\Omega}_i \\ \ldots \\ f_m : P_m \drarrow \boldsymbol{\Omega}_i}} (\tau_i \circ F\langle\seq{f}{m}\rangle \circ c_i)^*\boldsymbol{\Omega}_i \]
\uncover<2->{\textbf{Théorème :} $P \sqsubseteq l_i^\mathrm{sol}$ ssi} \\ \qquad\qquad\qquad \uncover<3->{$(i,P)$ position gagnante dans un jeu de parité}
......@@ -363,7 +365,7 @@
\vspace{10pt}
\item<3-> transferts des solutions entre fibrations
\vspace{10pt}
\item<4-> vérification de modèles pour la logique modale coalgébrique (à paraître)
\item<4-> vérification de modèles pour la logique modale coalgébrique
\end{itemize}
\end{frame}
......@@ -474,6 +476,7 @@
\textbf{Théorème :} $P \sqsubseteq l_i^\mathrm{sol}$ ssi $(i,P)$ est gagnante dans un jeu de parité
}
\vspace{10pt}
\uncover<3->{
Exemple : montrer que la solution est symétrique
}
......@@ -514,7 +517,7 @@
\vspace{10pt}
\item<3-> vérification de modèles pour la logique modale coalgébrique (à paraître)
\vspace{10pt}
\item<4-> pas de réussite pour exprimer les bisimulations pour automates de B\"uchi \uncover<5->{ mais une méthode de preuve intéressante }
\item<4-> tentative d'exprimer les bisimulations pour automates de B\"uchi \uncover<5->{avec une méthode de preuve assez puissante }
\end{itemize}
\end{frame}
......@@ -526,9 +529,11 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\appendix
\section{Appendices}
\begin{frame}
\begin{frame}[noframenumbering]
\sectionpage
\end{frame}
......@@ -559,7 +564,7 @@
\end{itemize}
\end{frame}
\begin{frame}
\begin{frame}[noframenumbering]
\frametitle{Ébauche de preuve du théorème}
\begin{enumerate}
\item $P \sqsubseteq l_i^\mathrm{sol}$
......@@ -572,7 +577,7 @@
\end{enumerate}
\end{frame}
\begin{frame}
\begin{frame}[noframenumbering]
\frametitle{Un autre jeu pour les systèmes d'équations \tiny
[Baldan+, CONCUR'20]}
\begin{align*}
......
......@@ -9,7 +9,7 @@
keywords = {_tablet}
}
@article{baldanAbstractionUptoTechniques2020,
@online{baldanAbstractionUptoTechniques2020,
title = {Abstraction, {{Up}}-to {{Techniques}} and {{Games}} for {{Systems}} of {{Fixpoint Equations}}},
author = {Baldan, Paolo and König, Barbara and Padoan, Tommaso},
date = {2020-03-19},
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment