Commit 2aa85c8a authored by Quentin Aristote's avatar Quentin Aristote
Browse files

small corrections

parent 12537707
\documentclass{beamer}
\usecolortheme{seahorse}
\setbeamertemplate{footline}[frame number]
\setbeamertemplate{navigation symbols}{}
% \setbeamertemplate{navigation symbols}{}
\usepackage{amsmath}
\usepackage{amssymb}
......@@ -63,8 +63,8 @@
\begin{figure}[h]
\centering
\begin{tikzpicture}
\uncover<2->{
\begin{scope}[every node/.style={state,thick,scale=0.5}]
\uncover<3->{
\begin{scope}[every node/.style={state,scale=0.5}]
\node (A) at (0,0) {} ;
\node (B) at (3,1) {} ;
\node (C) at (3,-1) {} ;
......@@ -95,48 +95,53 @@
}
\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) {} ;
\node<4-5> (B) at (3,1) {} ;
\node<4> (C) at (3,-1) {} ;
\node<5-> (E) at (6,-.5) {} ;
\node<6> (D) at (6,1) {} ;
\node<7> (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) ;
\path<5-> [->] (C) edge (E) ;
\path<7-> [->] (D) edge (H) ;
\end{scope}
\begin{scope}[every edge/.style={draw=blue,very thick}]
\path<5-> [->] (B) edge (D) ;
\path<6-> [->] (B) edge (D) ;
\end{scope}
\uncover<7->{
\begin{scope}[every node/.style={state,accepting,thick,scale=0.5}]
\uncover<8->{
\begin{scope}[every node/.style={state,accepting,scale=0.5}]
\node (B) at (3,1) {} ;
\node (E) at (6,-.5) {} ;
\node (F) at (6,-1.5) {} ;
\end{scope}
}
\uncover<8->{
\uncover<9->{
\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}]
\begin{scope}[every node/.style={state,accepting,scale = .25,right}]
\node at (0,-.5) {} ;
\node at (3,-1.5) {} ;
\end{scope}
}
\end{tikzpicture}
\end{figure}
\uncover<2-7>{
\[ c : X \rightarrow \mathcal{P}(X) \]
}
\uncover<8->{
\[ c : X \rightarrow FX \]
}
\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.
% programme représenté par un système de transitions : <2> typiquement fonction qui a un état associe les possibles états suivants -> <3> automate (etiquetté), chaine de markov, etc.
% définition bisimulation par théorie des jeux : <4> un joueur propose une transition depuis un état, <5> l'autre joueur répond avec une transition depuis l'autre état, <6> et on recommence infiniment ; si le second joueur peut toujours jouer les états sont bisimilaires
% peut être défini pour des systèmes plus complexes : <7> ajouter des états finaux, 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
......@@ -175,9 +180,8 @@
}
\uncover<5->{
\node (P) at (2,1.5) {$P$} ;
\path [->] (P) edge node[below] {$g$} (Q) ;
\path [->] (P) edge node[below] {$f$} node[above] {.} (Q) ;
\node[rotate = 90] at (2,2) {$\sqsubseteq$} ;
\node[below] at (4,0) {$= p(g)$} ;
}
\end{tikzpicture}
\end{figure}
......@@ -186,11 +190,11 @@
\begin{table}[h]
\centering
\begin{tabular}{c c c c}
Fibration & $\mathbb{C}_X$ & $k : (X,P) \drarrow (Y,Q)$ ssi & $f^*Q$ \\
Fibration & $\mathbb{C}_X$ & $f : P \drarrow Q$ ssi & $f^*Q$ \\
\toprule
\uncover<7->{$\Pred{}$ & $\Omega^X$ & $P \sqsubseteq Q \circ k$ & $Q \circ k$} \\
\uncover<7->{$\Pred{}$ & $\Omega^X$ & $P \sqsubseteq Q \circ f$ & $Q \circ f$} \\
\midrule
\uncover<8->{$\ERel{}$ & $\Omega^{X^2}$ & $P \sqsubseteq Q \circ (k \times k)$ & $Q \circ (k \times k)$} \\
\uncover<8->{$\ERel{}$ & $\Omega^{X^2}$ & $P \sqsubseteq Q \circ (f \times f)$ & $Q \circ (f \times f)$} \\
\midrule
\uncover<9->{$\mathbf{Pmet}_1$ & & $\cdots$ &} \\
\midrule
......
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