\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$

.PS
copy "macros.pic"
copy "vending.pic"
.PE
\thepicture



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

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

\adviwait
.PS
copy "macros.pic"
copy "vending1.pic"
.PE
\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$

.PS
copy "macros.pic"
copy "vending2.pic"
.PE
\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}


