\newif\ifslides\slidestrue
% \newif\ifslides\slidesfalse

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{mon-seminar}
\input{mon-color}
\input{mon-dvipdf}
\usepackage{eurosym}

\usepackage{hyperref}
% \usepackage {pstcol,color,pst-node}
\usepackage{advi}
\usepackage{advi-annot}
\usepackage{advi-graphicx}
\usepackage{superpose}
\usepackage{amssymb}

\newcommand{\urlter}[3]{\advirecord{#1}{%
\adviembed[name=netscape; height=0mm]{%
netscape -remote openFile(#2)}}%
\advianchor[click]{#1}{#3}%
}
\newcommand{\urlbis}[2]{\advirecord{#1}{%
\adviembed[name=netscape; height=0mm]{%
netscape -remote openURL(#2)}}%
\advianchor[click]{#1}{\url{#2}}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\newif\ifFrenchItemizeSpacing \FrenchItemizeSpacingfalse
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\WHILE}{\mbox{\sf\colorKeyword while}\;}
\newcommand{\DO}{\;\mbox{\sf\colorKeyword do}\;}
\newcommand{\AND}{\;\mbox{\sf\colorKeyword and}\;}
\newcommand{\OR}{\;\mbox{\sf\colorKeyword or}\;}
\newcommand{\WAIT}{\;\mbox{\sf\colorKeyword wait}\;}
\newcommand{\IF}{\;\mbox{\sf\colorKeyword if}\;}
\newcommand{\THEN}{\;\mbox{\sf\colorKeyword then}\;}
\newcommand{\ELSE}{\;\mbox{\sf\colorKeyword else}\;}
\newcommand{\BEGIN}{\;\mbox{\sf\colorKeyword begin}\;}
\newcommand{\END}{\;\mbox{\sf\colorKeyword end}\;}
\newcommand{\pair}[2]{\langle #1,\; #2 \rangle}
\newcommand{\SKIP}{\mbox{\sf\colorKeyword skip}\;}
\newcommand{\TRUE}{\mbox{\sf\colorKeyword true}\;}
\newcommand{\FALSE}{\mbox{\sf\colorKeyword false}\;}
\newcommand{\AWAIT}{\mbox{\sf\colorKeyword await}\;}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\turn}{\mbox{\em turn}}
\newcommand{\ass}{:=}
\newcommand{\para}{\mid\mid}
\newcommand{\tab}[3]{\multicolumn{#1}{l}{}&
                     \multicolumn{#2}{l}{{#3}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \bfseries
\blueSky
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\begin{center}
{\blueBis \huge \bf Concurrency 2 \\[1ex]
\colorbox{monyellow}{Functions vs Processes}\\[.3ex]
\colorbox{monyellow}{$\Rightarrow$ Interaction}\\[.3ex]
}
\bigskip
{\red Jean-Jacques L�vy}\\[2ex]


{\small\ahref{http://jeanjacqueslevy.net/dea}{jeanjacqueslevy.net/dea}}\\[2ex]

\end{center}

\end{slide}
\blueSky
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\centerslidesfalse
\newcommand{\tleft}{[\hspace{-.3ex}[}
\newcommand{\tright}{]\hspace{-.3ex}]}

\begin{slide}{}
\heading{Concurrency $\Rightarrow$ Non-deterministism}

Suppose $x$ is a global variable. 
At beginning, $x=0$

Consider\\[1ex]
 $P = [x \ass x+1; x \ass x+1  \para x\ass 2*x]$  

after $P$, then
$x$ may have several values  ($x \in \{ 2, 3, 4 \})$

Hence $P$ is not a function from memory states to memory states.

\adviwait
\bigskip

In concurrent programming, execution is {\red not deterministic} since
it is upto an external agent (the scheduler).

\adviwait
\bigskip

Let $\Sigma = \mbox{Variables} \mapsto \mbox{Values}$ be the set of
memory states. \\
Let $\tleft P \tright$ be the meaning of $P$. 

A concurrent program is not a (partial) function from memory states to
memory states. $\tleft P \tright \not\in \Sigma \mapsto \Sigma$.

A concurrent program is a {\orchidBis relation} on memory states.
$\tleft P \tright \in \Sigma \mapsto 2^\Sigma$.

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}{}
\heading{Concurrency $\Rightarrow$ Interaction}

Consider\\[1ex]
 $P = [x \ass 1 ]$ \\ 
 $Q = [x \ass 0; x \ass x+1 ]$ \\

$P$ and $Q$ are same functions on memory states: $\sigma \mapsto 
\sigma[1/x]$

\adviwait
\bigskip

However\\[1ex]
after $P \para P$, then $x \in \{ 1 \}$ \\
after $P \para Q$, then $x \in \{1,2\}$ 

\adviwait
\bigskip

A semantic (meaning) is {\DarkOrange compositional} iff 
$\tleft P \tright = \tleft Q \tright$ implies
$\tleft\; C[P] \;\tright = \tleft\; C[Q] \;\tright$
for any context $C[\;]$.

\adviwait
\bigskip

In previous example, 
in any compositional semantics, 
$\tleft P \tright \neq \tleft Q \tright$.

\bigskip

Conclusion\\[1ex]
$P$ and $Q$ are {\red not} equivalent processes.



\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Concurrency $\Leftrightarrow$ Termination}


Concurrent processes are often {\red non terminating}. 

An operating system never terminates; same for the software of 
a vending machine, or a traffic-light controler, or a human, etc.

\adviwait
\bigskip

A process $P$ is a set of pairs $(f_i, P_i)$, atomic action and a
derivative process. It starts by performing $f_i$ and then becomes process
$P_i$.

Atomic steps usually terminate.

\adviwait
\bigskip\bigskip

Roughly speaking, let $\mathcal P$ be the set of processes.
Then
$\mathcal P = 2^{(\Sigma \mapsto \Sigma) \times \mathcal P}$

\bigskip

\adviwait
Is this equation meaningful? Answer: Scott's domains, denotational
semantics. Remarkable and difficult theory of Plotkin (Scott's
powerdomains 1976).

We try the simpler theory of labeled transition systems.

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\processes}{\mathcal{P}}
\newcommand{\actions}{\mathcal{A}ct}
\newcommand{\transitions}{\mathcal{T}}
\renewcommand{\goes}[1]{\stackrel{#1}{\longrightarrow}}

\begin{slide}{}
\heading{Labeled Transition Systems}

A LTS is triple $(\processes, \actions, \transitions)$ where

\begin{itemize}
\item 
$\processes$ is the set of processes

\item
$\actions$ is the set of actions

\item
$\transitions \subseteq \processes \times \actions \times \processes$
is the transition relation
\end{itemize}

\bigskip
Let write $P \goes{\mu} Q$ for $(P, \mu, Q) \in \transitions$.\\
Read $P$ interacts with environment with action $\mu$, then becomes $Q$.

\bigskip

$Q$ is a {\red derivative} of $P$ if 
$P=P_0 \goes{\mu_1} P_1 \goes{\mu_2} P_2 \cdots \goes{\mu_n} P_n=Q$
for $n \geq 0$. 




\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Example (1/3)}

A vending machine for coffee/tea.
At beginning, $P_0$

%%BEGIN IMAGE
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 111 731 111 111 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.731in
    \rlap{\kern 0.111in\lower\graphtemp\hbox to 0pt{\hss $P_0$\adviwait\hss}}%
    \special{pa 222 731}%
    \special{pa 886 731}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 786 706}%
    \special{pa 886 731}%
    \special{pa 786 756}%
    \special{pa 786 706}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.660in
    \rlap{\kern 0.554in\lower\graphtemp\hbox to 0pt{\hss \small  .20\euro\hss}}%
    \special{ar 997 731 111 111 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.731in
    \rlap{\kern 0.997in\lower\graphtemp\hbox to 0pt{\hss $P_1$\adviwait\hss}}%
    \special{pa 1088 667}%
    \special{pa 1792 175}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1695 212}%
    \special{pa 1792 175}%
    \special{pa 1724 253}%
    \special{pa 1695 212}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.350in
    \rlap{\kern 1.390in\lower\graphtemp\hbox to 0pt{\hss \small  coffee \hspace{1ex}\hss}}%
    \special{ar 1883 111 111 111 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.111in
    \rlap{\kern 1.883in\lower\graphtemp\hbox to 0pt{\hss $P_2$\adviwait\hss}}%
    \special{pa 1772 111}%
    \special{pa 820 111}%
    \special{pa 195 658}%
    \special{sp}%
    \special{sh 1.000}%
    \special{pa 286 611}%
    \special{pa 195 658}%
    \special{pa 254 573}%
    \special{pa 286 611}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.038in
    \rlap{\kern 1.081in\lower\graphtemp\hbox to 0pt{\hss drink\adviwait\hss}}%
    \special{pa 1088 795}%
    \special{pa 1792 1288}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1724 1210}%
    \special{pa 1792 1288}%
    \special{pa 1695 1251}%
    \special{pa 1724 1210}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.970in
    \rlap{\kern 1.489in\lower\graphtemp\hbox to 0pt{\hss \small  tea\hss}}%
    \special{ar 1883 1351 111 111 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 1.351in
    \rlap{\kern 1.883in\lower\graphtemp\hbox to 0pt{\hss $P_3$\adviwait\hss}}%
    \special{pa 1772 1351}%
    \special{pa 820 1351}%
    \special{pa 195 804}%
    \special{sp}%
    \special{sh 1.000}%
    \special{pa 254 889}%
    \special{pa 195 804}%
    \special{pa 286 851}%
    \special{pa 254 889}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.424in
    \rlap{\kern 1.081in\lower\graphtemp\hbox to 0pt{\hss drink\hss}}%
    \hbox{\vrule depth1.462in width0pt height 0pt}%
    \kern 1.994in
  }%
}%
%%END IMAGE
\thepicture



\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Example (2/3)}

A different vending machine for coffee/tea.
At beginning, $P_0'$

\adviwait
%%BEGIN IMAGE
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 111 731 111 111 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.731in
    \rlap{\kern 0.111in\lower\graphtemp\hbox to 0pt{\hss $P_0'$\hss}}%
    \special{pa 222 731}%
    \special{pa 886 731}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 786 706}%
    \special{pa 886 731}%
    \special{pa 786 756}%
    \special{pa 786 706}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.660in
    \rlap{\kern 0.554in\lower\graphtemp\hbox to 0pt{\hss \small  .20\euro\hss}}%
    \special{ar 997 731 111 111 0 6.28319}%
    \special{pa 1088 667}%
    \special{pa 1792 175}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1695 212}%
    \special{pa 1792 175}%
    \special{pa 1724 253}%
    \special{pa 1695 212}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.350in
    \rlap{\kern 1.390in\lower\graphtemp\hbox to 0pt{\hss \small  coffee \hspace{1ex}\hss}}%
    \special{ar 1883 111 111 111 0 6.28319}%
    \special{pa 1974 175}%
    \special{pa 2678 667}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2610 590}%
    \special{pa 2678 667}%
    \special{pa 2581 631}%
    \special{pa 2610 590}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.350in
    \rlap{\kern 2.375in\lower\graphtemp\hbox to 0pt{\hss \small  drink\hss}}%
    \special{ar 2769 731 111 111 0 6.28319}%
    \special{pa 2657 731}%
    \special{pa 1108 731}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1208 756}%
    \special{pa 1108 731}%
    \special{pa 1208 706}%
    \special{pa 1208 756}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.643in
    \rlap{\kern 1.883in\lower\graphtemp\hbox to 0pt{\hss \small  .20\euro\hss}}%
    \special{ar 997 731 111 111 0 6.28319}%
    \special{pa 1088 795}%
    \special{pa 1792 1288}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1724 1210}%
    \special{pa 1792 1288}%
    \special{pa 1695 1251}%
    \special{pa 1724 1210}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.086in
    \rlap{\kern 1.409in\lower\graphtemp\hbox to 0pt{\hss \small  tea\hss}}%
    \special{ar 1883 1351 111 111 0 6.28319}%
    \special{pa 1974 1288}%
    \special{pa 2678 795}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2581 832}%
    \special{pa 2678 795}%
    \special{pa 2610 873}%
    \special{pa 2581 832}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.086in
    \rlap{\kern 2.357in\lower\graphtemp\hbox to 0pt{\hss \small  drink\hss}}%
    \hbox{\vrule depth1.462in width0pt height 0pt}%
    \kern 2.880in
  }%
}%
%%END IMAGE
\thepicture

\adviwait
Is this LTS equivalent to previous one?

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Example (3/3)}

Two new vending machines $P''_0$ and $P'''_0$

%%BEGIN IMAGE
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \graphtemp=.5ex\advance\graphtemp by 0.731in
    \rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss \adviwait\hss}}%
    \special{pn 8}%
    \special{ar 111 731 111 111 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.731in
    \rlap{\kern 0.111in\lower\graphtemp\hbox to 0pt{\hss $P_0''$\hss}}%
    \special{pa 214 690}%
    \special{pa 776 463}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 674 477}%
    \special{pa 776 463}%
    \special{pa 692 523}%
    \special{pa 674 477}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.505in
    \rlap{\kern 0.473in\lower\graphtemp\hbox to 0pt{\hss \small  .20\euro\hss}}%
    \special{ar 879 421 111 111 0 6.28319}%
    \special{pa 982 380}%
    \special{pa 1544 153}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1441 167}%
    \special{pa 1544 153}%
    \special{pa 1460 213}%
    \special{pa 1441 167}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.195in
    \rlap{\kern 1.241in\lower\graphtemp\hbox to 0pt{\hss \small  coffee \hspace{1ex}\hss}}%
    \special{ar 1647 111 111 111 0 6.28319}%
    \special{pa 1535 111}%
    \special{pa 495 111}%
    \special{pa 170 637}%
    \special{sp}%
    \special{sh 1.000}%
    \special{pa 243 565}%
    \special{pa 170 637}%
    \special{pa 201 539}%
    \special{pa 243 565}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.017in
    \rlap{\kern 0.630in\lower\graphtemp\hbox to 0pt{\hss drink\hss}}%
    \special{pa 214 773}%
    \special{pa 776 1000}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 692 939}%
    \special{pa 776 1000}%
    \special{pa 674 985}%
    \special{pa 692 939}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.930in
    \rlap{\kern 0.482in\lower\graphtemp\hbox to 0pt{\hss \small  .20\euro\hss}}%
    \special{ar 879 1041 111 111 0 6.28319}%
    \special{pa 982 1083}%
    \special{pa 1544 1310}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1460 1249}%
    \special{pa 1544 1310}%
    \special{pa 1441 1295}%
    \special{pa 1460 1249}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.125in
    \rlap{\kern 1.284in\lower\graphtemp\hbox to 0pt{\hss \small  tea\hss}}%
    \special{ar 1647 1351 111 111 0 6.28319}%
    \special{pa 1535 1351}%
    \special{pa 495 1351}%
    \special{pa 170 826}%
    \special{sp}%
    \special{sh 1.000}%
    \special{pa 201 924}%
    \special{pa 170 826}%
    \special{pa 243 898}%
    \special{pa 201 924}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.446in
    \rlap{\kern 0.630in\lower\graphtemp\hbox to 0pt{\hss drink\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.731in
    \rlap{\kern 1.758in\lower\graphtemp\hbox to 0pt{\hss \adviwait\hss}}%
    \special{ar 2369 731 111 111 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.731in
    \rlap{\kern 2.369in\lower\graphtemp\hbox to 0pt{\hss $P_0'''$\hss}}%
    \special{pa 2369 620}%
    \special{pa 2369 222}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2344 322}%
    \special{pa 2369 222}%
    \special{pa 2394 322}%
    \special{pa 2344 322}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.421in
    \rlap{\kern 2.326in\lower\graphtemp\hbox to 0pt{\hss \small  .20\euro\hss}}%
    \special{ar 2369 111 111 111 0 6.28319}%
    \special{pa 2480 731}%
    \special{pa 3025 731}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2925 706}%
    \special{pa 3025 731}%
    \special{pa 2925 756}%
    \special{pa 2925 706}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.660in
    \rlap{\kern 2.753in\lower\graphtemp\hbox to 0pt{\hss \small  .20\euro\hss}}%
    \special{ar 3136 731 111 111 0 6.28319}%
    \special{pa 3223 661}%
    \special{pa 3818 181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3724 224}%
    \special{pa 3818 181}%
    \special{pa 3756 263}%
    \special{pa 3724 224}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.350in
    \rlap{\kern 3.477in\lower\graphtemp\hbox to 0pt{\hss \small  coffee \hspace{1ex}\hss}}%
    \special{ar 3904 111 111 111 0 6.28319}%
    \special{pa 3793 111}%
    \special{pa 2983 111}%
    \special{pa 2447 652}%
    \special{sp}%
    \special{sh 1.000}%
    \special{pa 2535 599}%
    \special{pa 2447 652}%
    \special{pa 2500 564}%
    \special{pa 2535 599}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.032in
    \rlap{\kern 3.215in\lower\graphtemp\hbox to 0pt{\hss drink\hss}}%
    \special{pa 3223 801}%
    \special{pa 3818 1281}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3756 1199}%
    \special{pa 3818 1281}%
    \special{pa 3724 1238}%
    \special{pa 3756 1199}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.970in
    \rlap{\kern 3.563in\lower\graphtemp\hbox to 0pt{\hss \small  tea\hss}}%
    \special{ar 3904 1351 111 111 0 6.28319}%
    \special{pa 3793 1351}%
    \special{pa 2983 1351}%
    \special{pa 2447 810}%
    \special{sp}%
    \special{sh 1.000}%
    \special{pa 2500 899}%
    \special{pa 2447 810}%
    \special{pa 2535 864}%
    \special{pa 2500 899}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.430in
    \rlap{\kern 3.215in\lower\graphtemp\hbox to 0pt{\hss drink\hss}}%
    \hbox{\vrule depth1.462in width0pt height 0pt}%
    \kern 4.015in
  }%
}%
%%END IMAGE
\thepicture

\adviwait
\bigskip
Why these LTS are not equivalent to previous ones?

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\traces}{\mathop{\mathit{\mathcal{T}\hspace{-.5ex}races}}}
\newcommand{\trace}{\mathop{\mathit{trace}}}
\newcommand{\pref}{\mathop{\mathit{prefixes}}}

\begin{slide}{}
\heading{Concurrency $\Leftrightarrow$ Automata (1/2)}

Let abstract $\actions$ ({\red actions}) as an alphabet
$\{a, b, c, \ldots\}$. \\
($\actions$ may be infinite)

Then $LTS$ look like automata (with possibly infinite number of
states).

\bigskip
Consider the language of {\DarkOrange traces}.

Let $P=P_0 \goes{\mu_1} P_1 \goes{\mu_2} P_2 \cdots \goes{\mu_n} P_n$
($n \geq 0$), 
then

$\trace({P=P_0 \goes{\mu_1} P_1 \goes{\mu_2} P_2 \cdots \goes{\mu_n} P_n})
= \mu_1\mu_2\cdots\mu_n$

\bigskip
We say that $\mu_1\mu_2\cdots\mu_n$ is a trace of $P$

\bigskip
Let $\traces(P) = \{ w \mid w \;\mbox{is a trace of}\; P \}$

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Concurrency $\Leftrightarrow$ Automata (2/2)}

In previous examples, write $k$ for coffee, $t$ for tea, $c$ for
$.20\euro$, $d$ for drink.

$\traces(P_0) = \pref((c(k+t)d)^*)$,\\
$\traces(P'_0) = \pref(c((k+t)dc)^*)$,\\
$\traces(P''_0) = \pref((ckd + ctd)^*$,\\
$\traces(P'''_0) = \pref((c+c(k+t)dc)^*)$,\\

\adviwait
\exercice Show
$\traces(P_0) = \traces(P'_0) = \traces(P''_0) = \traces(P'''_0)$

\bigskip
\adviwait

However, $P_0$ and $P_0'$ seem equivalent\\
but both $P_0''$ and $P_0'''$ look distinct from $P_0$.

\bigskip
Why? 
\adviwait

After $c$, the set of choices are distinct in $P_0$ and $P''_0$.\\
Coffee button is always enabled in $P_0$, but not in $P''_0$.\\ Same
for tea button.\\

In $P'''_0$, both tea and coffee may be disabled after $c$. 

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Simulation -- Bisimulation}

\begin{definition}\label{def:bisim1}
$Q$ simulates $P$ (we write $P \lesssim Q$) if whenever
$P \goes{\mu} P'$, there is $Q'$ such that 
$Q \goes{\mu} Q'$ and $P' \lesssim Q'$.
\end{definition}

\begin{definition}
$P$ strongly bisimilar to $Q$ (we write $P \sim Q$) if whenever
\begin{itemize} 

\item 
$P \goes{\mu} P'$, there is $Q'$ such that 
$Q \goes{\mu} Q'$ and $P' \sim Q'$.

\item 
$Q \goes{\mu} Q'$, there is $P'$ such that 
$P \goes{\mu} P'$ and $P' \sim Q'$.

\end{itemize} 
\end{definition}

\bigskip
Graphically,

\vfill


\adviwait
\exercice Give intuition for $P_0 \lesssim P_0''' \lesssim P_0$

\exercice Give intuition for $P_0 \sim P_0'$, $P_0 \not\sim P_0''$,
$P_0 \not\sim P_0'''$

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\bisim}[1]{\mathrel{\mathcal{#1}}}

\begin{slide}{}
\heading{Definition of bisimulation (1/3)}

\begin{definition}
A bisimulation is a binary relation $\mathcal{R}$ on processes 
such that $P \bisim{R} Q$ implies whenever
\begin{itemize} 

\item 
$P \goes{\mu} P'$, there is $Q'$ such that 
$Q \goes{\mu} Q'$ and $P' \bisim{R} Q'$.

\item 
$Q \goes{\mu} Q'$, there is $P'$ such that 
$P \goes{\mu} P'$ and $P' \bisim{R} Q'$.

\end{itemize} 
\end{definition}

\bigskip

An alternative definition for strong bisimulation is:

\begin{definition}
Let $\sim \;=\; \cup \{\bisim{R} \;\mid\; \bisim{R} \;\mbox{is a
bisimulation}\}$
\end{definition}

\bigskip

\adviwait
\begin{prop}
$\sim$ is an equivalence relation.\\
(reflexive, symmetric, transitive)
\end{prop}


\adviwait
\exercice Show above proposition.

\adviwait
\exercice What is the least bisimulation?


\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\lfp}{\mathop{\mathtt{lfp}}}
\newcommand{\gfp}{\mathop{\mathtt{gfp}}}

\begin{slide}{}
\heading{Definition of bisimulation (2/3)}

First definition of bisimulation is {\red circular}. To make it clear,
better is to return to standard theory on fixpoints in complete
lattices.

A {\orchidBis complete lattice} $\mathcal{D}$ is any set with 
\begin{itemize}
\item a partial ordering $\preceq$  (reflexive, transitive, antisymmetric)
\item for any subset $E \subseteq D$, there is an upper bound $\cup E$
  and a lower bound $\cap E$ in $D$.
\end{itemize}

\bigskip

Examples: $2^\processes$ with $\subseteq$, 
$2^{\processes\times\processes}$ with $\subseteq$,  etc.

\bigskip
$f$ function $D \mapsto D$ is {\DarkOrange monotonic} iff $x \preceq
y$ implies $f(x) \preceq f(y)$.

\bigskip
\begin{thm}[{\red Tarski}]
In a complete lattice $D$, any monotonic function $f$ has a least
fixpoint $\lfp(f)$ and greatest fixpoint $\gfp(f)$.

Moreover $\lfp(f) = \cap\{x \mid f(x) \preceq x\}$
and $\gfp(f) = \cup\{x \mid x \preceq f(x)\}$
\end{thm}

\exercice Prove it.

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Definition of bisimulation (3/3)}

\begin{prop}
$\sim$ is the largest relation $\sim'$ such that
$P \sim' Q$ implies whenever
\begin{itemize} 

\item 
$P \goes{\mu} P'$, there is $Q'$ such that 
$Q \goes{\mu} Q'$ and $P' \sim' Q'$.

\item 
$Q \goes{\mu} Q'$, there is $P'$ such that 
$P \goes{\mu} P'$ and $P' \sim' Q'$.

\end{itemize} 
\end{prop}

\bigskip 
\adviwait
{\brownBis Proof}: Consider the complete lattice of binary relations on
$\processes$ with $\subseteq$.  
\adviwait
Take $P \;f(\bisim{R})\; Q$ defined as
whenever
\begin{itemize} 

\item 
$P \goes{\mu} P'$, there is $Q'$ such that 
$Q \goes{\mu} Q'$ and $P' \bisim{R} Q'$.

\item 
$Q \goes{\mu} Q'$, there is $P'$ such that 
$P \goes{\mu} P'$ and $P' \bisim{R} Q'$.

\end{itemize} 
\adviwait
Then $f$ is monotonic, since $\bisim{R} \subseteq \bisim{S}$
implies $f(\bisim{R}) \subseteq f(\bisim{S})$. 

\adviwait
Moreover $\bisim{R}$ is a bisimulation iff $\bisim{R} \subseteq
f(\bisim{R})$.

\adviwait
Hence $\sim\;=\;\cup\{\bisim{R} \;\mid\; \bisim{R} \;\subseteq\;
f(\bisim{R})\} \;=\; \gfp(f)$.

\adviwait
Therefore $\sim \;=\; f(\sim)$ and $\sim$ is largest $\sim'$ such
that $\sim' \;=\; f(\sim')$.
\bigskip

\adviwait
First definition of $\sim$ was correct (just add ``largest'').


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Co-induction}


In order to show $P \sim Q$, it is sufficient to show that
$P \bisim{R} Q$ for some bisimulation $\bisim{R}$.

I.e. $(P \bisim{R} Q$ for some relation $\bisim{R}$ such that
$\bisim{R} \;\subseteq f(\bisim{R})) \;\Rightarrow P\sim Q$.

\bigskip

\exercice Show $P_0 \sim P_0'$, $P_0 \not\sim P_0''$,
$P_0 \not\sim P_0'''$ in vending machines.

\exercice Give an alternative definition for $\lesssim$. 

\exercice Show $P_0 \lesssim P_0''' \lesssim P_0$.


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Co-continuity (1/2)}

Let $D$ be a complete lattice. Then

$f$ function $D \mapsto D$ is co-continuous iff $f(\cap S) =
\cap f(S)$ for any descending chain $S = \{d_1, d_2, \ldots d_n
\ldots \}$ where $d_1 \succeq d_2 \succeq \cdots \succeq d_n \succeq\cdots $

\begin{thm}[{\red Kleene}]
$\gfp(f) = \cap \{ f^n(\top) \mid n \geq 0 \}$ where $\top$ is maximum
element of $D$.
\end{thm}

\bigskip
\adviwait
Consider lattice of binary relations $2^{\processes\times\processes}$
with $\subseteq$. 

Let the graph of derivatives of $P$ be {\red finitely branching},
i.e.~$\{Q \mid P \goes{\mu} Q\}$ is finite for any $P$.

\adviwait
Take $P \;f(\bisim{R})\; Q$ defined as
whenever
\begin{itemize} 

\item 
$P \goes{\mu} P'$, there is $Q'$ such that 
$Q \goes{\mu} Q'$ and $P' \bisim{R} Q'$.

\item 
$Q \goes{\mu} Q'$, there is $P'$ such that 
$P \goes{\mu} P'$ and $P' \bisim{R} Q'$.

\end{itemize} 

Then $f$ is co-continuous.

\bigskip

If the graph of derivatives is finitely branching, then
$\sim \;=\; \cap \,\{ f^n(D) \mid n \geq 0 \}$

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Co-continuity (2/2)}

\exercice Suppose $P$ has a finite graph of derivatives. Give an
algorithm for computing its minimal graph of derivatives, i.e.\ a graph
where distinct states are not bisimilar.  \\
$O(n\log n)$ algorithm by Paige and Tarjan, \\
(analogous of Hopcroft/Ullman algorithm for
computing minimal finite automata).

\bigskip

\exercice Suppose $P$ and $Q$ have finite graphs of derivatives. Give an
algorithm for testing $P \sim Q$.

\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{Exercices}

\begin{definition}
$\bisim{R}$ is a bisimulation up-to $\sim$ if $P \bisim{R} Q$ implies
whenever
\begin{itemize} 

\item 
$P \goes{\mu} P'$, there is $Q'$ such that 
$Q \goes{\mu} Q'$ and $P' \sim\bisim{R}\sim Q'$.

\item 
$Q \goes{\mu} Q'$, there is $P'$ such that 
$P \goes{\mu} P'$ and $P' \sim\bisim{R}\sim Q'$.

\end{itemize} 

\end{definition}

\bigskip

\exercice Let $\bisim{R}$ is a bisimulation up-to $\sim$. Show
$\bisim{R} \;\subseteq\; \sim$.\\
(by firstly showing that $\sim\bisim{R}\sim$ is a bisimulation).

\bigskip
Let $\mu^+ \in \actions^+$ (not empty words of actions)

Write $P \goes{\mu^+} Q$ if 
$P=P_0 \goes{\mu_1} P_1 \goes{\mu_2} P_2 \cdots \goes{\mu_n} P_n=Q$
and $\mu = \mu_1\mu_2\cdots\mu_n$ ($n > 0$).

\bigskip

\exercice Show that following definition of strong bisimulation is 
equivalent to previous one.

\begin{definition}
$\bisim{R}$ is a (strong) bisimulation if $P \bisim{R} Q$ implies
whenever
\begin{itemize} 

\item 
$P \goes{\mu^+} P'$, there is $Q'$ such that 
$Q \goes{\mu^+} Q'$ and $P' \sim\bisim{R}\sim Q'$.

\item 
$Q \goes{\mu^+} Q'$, there is $P'$ such that 
$P \goes{\mu^+} P'$ and $P' \sim\bisim{R}\sim Q'$.

\end{itemize} 

\end{definition}


\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{}
\heading{History}

David Park invented bisimulation as maximal fixpoints. (1975)

Robin Milner wrote a full book on them for CCS. (1979)

Samson Abramsky added them in the lazy lambda calculus. (1984)
See also phD of his student Luke Ong.

Davide Sangiorgi did the theory of bisimulation in the
pi-calculus. (1990)

Marcelo Fiore et al put them in data types. (1992)

Many people speak now of bisimulations, as a generic names for
equivalences on infinite computations.

For instance, Dave Sands and others use them for equivalence of Bohm
trees in the lambda-calculus (which I never understood!!).

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}


