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

first three slides

1st slide : title page
2nd slide : bisimulations
3rd slide : fibrations
parent 3309c31f
\documentclass{beamer}
\usecolortheme{seahorse}
\setbeamertemplate{footline}[frame number]
\setbeamertemplate{navigation symbols}{}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage[french]{babel}
\usepackage{dsfont}
\usepackage{stmaryrd}
\usepackage{hyperref}
\usepackage{tikz-cd}
\usetikzlibrary{automata}
\usepackage{booktabs}
\usepackage{makecell}
\usepackage{tabularx}
\newcommand{\sem}[1]{\left\llbracket\,#1\,\right\rrbracket}
\newcommand{\clatfibration}{$\mathbf{CLat}_\sqcap$-fibration}
\newcommand{\Cmu}{$\mathbf{C\mu}_{\Gamma,\Lambda}$}
\newcommand{\seq}[3][1]{#2_{#1},\allowbreak\ldots,#2_{#3}}
\newcommand{\ellipsis}[5][\cdots]{#2_{#3}#4#1#4#2_{#5}} % chktex 11
\newcommand{\family}[3]{\left(#1_{#2}\right)_{#3}}
\newcommand{\place}{\underline{\phantom{n}}\,} % place holder
\newcommand{\drarrow}{\mathrel{\dot\rightarrow}}
\newcommand{\bigmid}{\ \middle|\ }
\newcommand{\Pred}[1][\Omega]{\mathbf{Pred}_{#1}}
\newcommand{\ERel}[1][\Omega]{\mathbf{ERel}_{#1}}
\DeclareMathOperator{\Obj}{Obj}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\Id}{Id}
\DeclareMathOperator{\pr}{pr}
\DeclareMathOperator{\new}{new}
\DeclareMathOperator{\sym}{sym}
% ChkTex parameters
% chktex-file 3
% chktex-file 18
% chktex-file 25
% chktex-file 36
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{Cadre fibrationnel pour point fixes imbriqués \\ \& \\Notions de (bi)simulations pour automates de B\"uchi}
\author{Quentin Aristote}
\date{}
\maketitle
% Bonjour
% je vais présenter mon stage qui portait sur <titre>
% objectif : généraliser résultats existants sur lien entre théorie des jeux et \nu d'un opérateur fibrationnel -> lien entre théorie des jeux et points fixes imbriqués dans fibrations
% résultats utilisés pour généraliser bisimulation (\nu) et lien avec théorie des jeux -> espoir de faire de même pour bisimulations pour automates de buchi (s'expriment seulement avec points fixes imbriqués)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Préliminaire : bisimulations}
\begin{figure}[h]
\centering
\begin{tikzpicture}
\uncover<2->{
\begin{scope}[every node/.style={state,thick,scale=0.5}]
\node (A) at (0,0) {} ;
\node (B) at (3,1) {} ;
\node (C) at (3,-1) {} ;
\node (D) at (6,1) {} ;
\node (E) at (6,-.5) {} ;
\node (F) at (6,-1.5) {} ;
\node (G) at (9,1.5) {} ;
\node (H) at (9,.5) {} ;
\node (I) at (9,-.5) {} ;
\node (J) at (9,-1.5) {} ;
\end{scope}
\begin{scope}[every node/.style={above}]
\path [->]
(A) edge node {a} (B)
(B) edge node {*} (D)
(D) edge node {a} (G)
(C) edge node {a} (E)
(E) edge node {a} (I) ;
\end{scope}
\begin{scope}[every node/.style={below}]
\path [->]
(A) edge node {b} (C)
(D) edge node {b} (H)
(C) edge node {b} (F)
(F) edge node {b} (J) ;
\end{scope}
}
\begin{scope}[every node/.style={state,very thick,scale=.5}]
\node<3-4> (B) at (3,1) {} ;
\node<3> (C) at (3,-1) {} ;
\node<4-> (E) at (6,-.5) {} ;
\node<5> (D) at (6,1) {} ;
\node<6> (H) at (9,.5) {} ;
\end{scope}
\begin{scope}[every edge/.style={draw=purple,very thick}]
\path<4-> [->] (C) edge (E) ;
\path<6-> [->] (D) edge (H) ;
\end{scope}
\begin{scope}[every edge/.style={draw=blue,very thick}]
\path<5-> [->] (B) edge (D) ;
\end{scope}
\uncover<7->{
\begin{scope}[every node/.style={state,accepting,thick,scale=0.5}]
\node (B) at (3,1) {} ;
\node (E) at (6,-.5) {} ;
\node (F) at (6,-1.5) {} ;
\end{scope}
}
\uncover<8->{
\begin{scope}[every node/.style={left}]
\node at (0,-.5) {$\exists$} ;
\node at (3,-1.5) {$\forall$} ;
\end{scope}
\begin{scope}[every node/.style={state,accepting,scale = .25,thick,right}]
\node at (0,-.5) {} ;
\node at (3,-1.5) {} ;
\end{scope}
}
\end{tikzpicture}
\end{figure}
\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
% programme représenté par un système de transitions (automate, chaine de markov, ...) <1>
% définition par théorie des jeux : un joueur propose une transition depuis un état, l'autre joueur répond avec une transition depuis l'autre état, et on recommence infiniment ; si le second joueur peut toujours jouer les états sont bisimilaires <3,4,5>
% peut être défini pour des systèmes plus complexes : ajouter des états finaux <2>, des probabilités de transitions , etc.
% résultat important : bisimilaires <=> vérifient les mêmes formules de logique modale
% logique modale : logique binaire + pour toute transition, il existe une transition
% résultats existants : écrire les bisimulations comme + grand point fixe d'un opérateur fibrationnel
% problème : certaines bisimulations (ex: automate buchi) ne s'écrivent qu'avec des points fixes imbriqués
% but : étendre les résultats pour prendre en compte les points fixes imbriqués
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Préliminaire : fibrations (de treillis complet)}
\begin{figure}[t]
\centering
\begin{tikzpicture}
\uncover<2->{
\node (C) at (0,2) {$\mathbb{C}$} ;
\node (B) at (0,0) {$\mathbb{B}$} ;
\path [->] (C) edge node[left] {$p$} (B) ;
}
\uncover<3->{
\node (X) at (2,0) {$X$} ;
\node (Y) at (6,0) {$Y$} ;
\begin{scope}[every circle/.style={x radius = .5, y radius = 1}]
\draw[dashed] (2,2) circle ;
\draw[dashed] (6,2) circle ;
\end{scope}
\begin{scope}[every node/.style={above}]
\node at (2,3) {$\mathbb{C}_X$} ;
\node at (6,3) {$\mathbb{C}_Y$} ;
\end{scope}
}
\uncover<4->{
\node (Q) at (6,2.5) {$Q$} ;
\node (fQ) at (2,2.5) {$f^*Q$} ;
\path [->] (X) edge node[above] {$f$} (Y) ;
\path [->] (fQ) edge node[above] {$\overline{f}Q$} (Q) ;
}
\uncover<5->{
\node (P) at (2,1.5) {$P$} ;
\path [->] (P) edge node[below] {$g$} (Q) ;
\node[rotate = 90] at (2,2) {$\sqsubseteq$} ;
\node[below] at (4,0) {$= p(g)$} ;
}
\end{tikzpicture}
\end{figure}
\uncover<6->{
\begin{table}[h]
\centering
\begin{tabular}{c c c c}
Fibration & $\mathbb{C}_X$ & $k : (X,P) \drarrow (Y,Q)$ ssi & $f^*Q$ \\
\toprule
\uncover<7->{$\Pred{}$ & $\Omega^X$ & $P \sqsubseteq Q \circ k$ & $Q \circ k$} \\
\midrule
\uncover<8->{$\ERel{}$ & $\Omega^{X^2}$ & $P \sqsubseteq Q \circ (k \times k)$ & $Q \circ (k \times k)$} \\
\midrule
\uncover<9->{$\mathbf{Pmet}_1$ & & $\cdots$ &} \\
\midrule
\uncover<9->{$\mathbf{Top}$ & & $\cdots$ &} \\
\bottomrule
\end{tabular}
\end{table}
}
\end{frame}
% je parle d'un opérateur fibrationnel : késako ?
% foncteur catégories totale -> base
% fibré (= préimage) est un treillis complet (= ensemble ordonné pour lequel on peut prendre le borne inférieure ou supérieure de n'importe quel sous ensemble)
% muni d'une opération : relèvement cartésien
%%%%%%%%%%%%%%%%%%%%%%%% si f : X -> Y et Q \in E_Y, \overline{f}(Q) : f^*Q -> Q le plus grand objet tel que f : P \darrow Q (pour lequel il existe g : P -> Q qui se projette sur f)
% relèvement conserve la borne inférieure et la composition
% exemples (catégorie base = ensembles) :
% Pred : - \Omega treillis complet
%%%%%%%% - objets fonctions X -> \Omega
%%%%%%%% - flèches fonction k : X -> Y tq P \sqsubseteq Q \circ k
%%%%%%%% - k^*Q = Q \circ k
% Rel : - objets relations X^2 -> \Omega
%%%%%%%% - flèches fonction k : X -> Y tq P \sqsubseteq Q \circ (k \times k)
%%%%%%%% - k^*Q = Q \circ (k \times k)
% Espaces métriques
% Espaces topologiques
% on peut généraliser un concept à d'autres fibrations en changeant le relèvement cartésien
\end{document}
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