\documentclass{beamer}

\usepackage{graphicx}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Pierre-Louis and Catuscia
\newcommand{\seq}[2]{\frac{#1}{#2}}
\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\cpl}[1]{#1^{c}}
\newcommand{\recgen}[1]{{\it letrec}\;\vec{K}=\vec{P}\;in #1}
\newcommand{\recone}[2]{{\it rec}\: #1.#2}
\newcommand{\outpt}[2]{#1\langle#2\rangle}
\newcommand{\sred}[1]{\;\stackrel{#1}{\rightarrow}\;}
\newcommand{\lsred}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\wred}[1]{\stackrel{#1}{\Rightarrow}}
\newcommand{\lwred}[1]{\stackrel{#1}{\Longrightarrow}}
\newcommand{\letin}[2]{{\it let}\;#1\;{\it in}\;#2}
\newcommand{\defin}[3]{{\it def}\:#1\rhd #2\:{\it in}\:#3}
\newcommand{\heat}{\leftrightharpoons}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% JJ and Catuscia
\colorlet{lightblue}{white!25!blue}
\colorlet{darkgreen}{black!50!green}
\newcommand{\WHILE}{\mbox{\sf \textcolor{lightblue}{while}}\;}
\newcommand{\DO}{\;\mbox{\sf\textcolor{lightblue}{do}}\;}
\newcommand{\AND}{\;\mbox{\sf\textcolor{lightblue}{and}}\;}
\newcommand{\OR}{\;\mbox{\sf\textcolor{lightblue}{or}}\;}
\newcommand{\IF}{\;\mbox{\sf\textcolor{lightblue}{if}}\;}
\newcommand{\THEN}{\;\mbox{\sf\textcolor{lightblue}{then}}\;}
\newcommand{\ELSE}{\;\mbox{\sf\textcolor{lightblue}{else}}\;}
\newcommand{\BEGIN}{\;\mbox{\sf\textcolor{lightblue}{begin}}\;}
\newcommand{\END}{\mbox{\sf\textcolor{lightblue}{end}}\;}
\newcommand{\pair}[2]{\langle #1,\; #2 \rangle}
\newcommand{\SKIP}{\mbox{\sf\textcolor{lightblue}{skip}}\;}
\newcommand{\TRUE}{\mbox{\sf\textcolor{lightblue}{true}}\;}
\newcommand{\FALSE}{\mbox{\sf\textcolor{lightblue}{false}}\;}
\newcommand{\AWAIT}{\mbox{\sf\textcolor{lightblue}{await}}\;}

%\newcommand{\REC}{\mbox{\sf\textcolor{lightblue}{rec}}}
\newcommand{\REC}{\mbox{\sf{rec}}}
\newcommand{\LET}{\mbox{\sf\textcolor{lightblue}{let}}\;}
\newcommand{\IN}{\mbox{\sf\textcolor{lightblue}{\;in}}\;}
\newcommand{\CLASS}{\mbox{\sf\textcolor{lightblue}{class}}\;}
\newcommand{\SYNCHRONIZED}{\mbox{\sf\textcolor{lightblue}{synchronized}}\;}
\newcommand{\PUBLIC}{\mbox{\sf\textcolor{lightblue}{public}}\;}
\newcommand{\PRIVATE}{\mbox{\sf\textcolor{lightblue}{private}}\;}
\newcommand{\VOID}{\mbox{\sf\textcolor{lightblue}{void}}\;}
\newcommand{\WAIT}{\;\mbox{\sf\textcolor{lightblue}{wait}}}
\newcommand{\NOTIFY}{\;\mbox{\sf\textcolor{lightblue}{notify}}}
\newcommand{\NOTIFYALL}{\;\mbox{\sf\textcolor{lightblue}{notifyAll}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\turn}{\mbox{\em turn}}
\newcommand{\ass}{:=}
\newcommand{\para}{\mid\mid}
\newcommand{\tab}[3]{\multicolumn{#1}{l}{}&
                     \multicolumn{#2}{l}{{#3}}}
\newcommand{\pic}{$\pi$-calculus}
\newcommand{\acquire}{\mathop{\mathit{acquire}}}
\newcommand{\release}{\mathop{\mathit{release}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\assert}[1]{{\textcolor{violet}{\{#1\}}}}
\newcommand{\actif}{\mathop{\it actif}}
\newcommand{\tour}{\mathop{\it turn}}
\newcommand{\CO}{\mathit{pc}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>
{
  \usetheme{Darmstadt}  
  %\usetheme{Warsaw}
  % or ...

  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}

\usecolortheme{seahorse}


\usepackage[english]{babel}
% or whatever

\usepackage[latin1]{inputenc}
% or whatever

\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.


\title[Concurrency 4] % (optional, use only with long paper titles)
{Concurrency 4}

\subtitle{CCS - Simulation and bisimulation. Coinduction.}

\author[Catuscia Palamidessi]{Catuscia Palamidessi\\
INRIA Futurs and LIX - Ecole Polytechnique}

%\institute[INRIA and LIX] % (optional, but mostly needed)
%{
%  INRIA Futurs and LIX - Ecole Polytechnique 
%}
% - Use the \inst command only if there are several affiliations.
% - Keep it simple, no one is interested in your street address.

\institute{The other lecturers for this course: }
\date{
Jean-Jacques L\'evy (INRIA Rocquencourt)\\
James Leifer (INRIA Rocquencourt)\\
Eric Goubault (CEA)\\ [2ex]
{\tt \scriptsize http://pauillac.inria.fr/\~{ }leifer/teaching/mpri-concurrency-2005/}
}
% - Either use conference name or its abbreviation.
% - Not really informative to the audience, more for people (including
%   yourself) who are reading the slides online

\subject{Course on Concurrency at MPRI}
% This is only inserted into the PDF information catalog. Can be left
% out. 



% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}


% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
\AtBeginSubsection[]
{
  \begin{frame}<beamer>
    \frametitle{Outline}
    \tableofcontents[currentsection,currentsubsection]
  \end{frame}
}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}


\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \titlepage
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Announcement} 
The class of Wednesday 26 October will follow the usual schedule (16h15 - 19h15). 
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{Outline}
  \tableofcontents
  % You might wish to add the option [pausesections]
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Solution to exercises from previous time}
\begin{frame}
\frametitle{The semaphore}
Define in CCS a semaphore with initial value $n$
\pause
\begin{block}{First Solution}{\scriptsize
$$\REC_{S_n} {\it down}.\REC_{S_{n-1}}({\it up}.S_n + {\it down}.\REC_{S_{n-2}}(\ldots ({\it up}.S_{2} + {\it down}.\REC_{S_0} {\it up}. S_1)\ldots ))
$$}
\end{block}
\pause
\begin{block}{Second solution}{\scriptsize
\begin{itemize}
\item Let $S = \REC_X {\it down}.{\it up}.X$
\vskip 3mm
\item Then $S_n = S \;|\; S \; | \; \ldots \;|\; S $  \ \ \ $n$ \  times
\end{itemize}}
\end{block}
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Maximal trace equivalence is not a congruence}
\pause
Consider the following processes
\begin{itemize}
\item \textcolor{purple}{$P = a.(b.0 + c.0)$}
\item \textcolor{blue}{$Q = a.b.0 + a.c.0$}
\item $R = \bar{a}. \bar{b}. \bar{d}. 0$
\end{itemize}
\vskip 3mm
\textcolor{purple}{$P$} and \textcolor{blue}{$Q$} have the same maximal traces, but $(\nu a) (\nu b)(\nu c)(\textcolor{purple}{P}\;|\;R)$ and $(\nu a) (\nu b)(\nu c)(\textcolor{blue}{Q}\;|\;R)$
have different maximal traces.
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Modern definition of CCS (1999)}
\subsection{Syntax}
\begin{frame}
\frametitle{Syntax of ``modern'' CCS}
{\footnotesize
\begin{itemize}
\item \textcolor{purple}{(channel, port) names}: \; $a, b, c, \ldots$
\item \textcolor{purple}{co-names}: \; $\bar a, \bar b, \bar c, \ldots$  \qquad Note: \; $\bar{\bar a} = a$
\item \textcolor{purple}{silent action}: \; $\tau$
\vskip 3mm
\item \textcolor{purple}{actions, prefixes}: $\mu\; \mbox{::=}\;\; a\;\;|\;\;\bar a \;\;|\;\; \tau$ 
\vskip 3mm
\item \textcolor{purple}{processes}: 
$\begin{array}[t]{lcll}
 P, Q &\mbox{::=} & 0 &\mbox{\textcolor{darkgreen}{inaction}}\\
      & | & \mu. P &\mbox{\textcolor{darkgreen}{prefix}}\\
      & | & P\,\mid\,Q  &\mbox{\textcolor{darkgreen}{parallel}}\\
      & | & P+Q  &\mbox{\textcolor{darkgreen}{(external) choice}}\\
      & | &  (\nu a) P &\mbox{\textcolor{darkgreen}{restriction}}\\
      & | &  \textcolor{violet}{ {K(\vec{a})}} &\mbox{\textcolor{violet}{process name with parameters}}\\
\end{array}$
\vskip 3mm
\pause
\item   \textcolor{violet}{Process definitions:}
$\begin{array}[t]{lcll}
 \textcolor{violet}{ D} &\mbox{ \textcolor{violet}{::=}} &  \textcolor{violet}{K(\vec{x}) \stackrel{def}{=} P } & \mbox{ \textcolor{violet}{where P may contain only the $\vec{x}$}}\\
  & &                                            & \mbox{ \textcolor{violet}{as channel names}}
\end{array}$
\end{itemize}
}
\end{frame}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Labeled transition System}
\begin{frame}
\frametitle{Labeled transition system for ``modern'' CCS}
{\small We assume a given set of definitions $D$
\vskip 3mm

$$\begin{array}{cc}
\; [\mbox{\scriptsize Act}] \;\; \frac{}{\mu.P\sred{\mu}P}
 & [\mbox{\scriptsize Res}]\;\;\frac{P\sred{\mu}P'\quad{\textcolor{darkgreen}{ \mu\neq a , \ol{a}}}}{(\nu a) P\sred{\mu}(\nu a)P'}\\
\; &\;\\
\; [\mbox{\scriptsize Sum1}]\;\;
\seq{P\sred{\mu} P'}{P+ Q\sred{\mu}P'}
&
[\mbox{\scriptsize Sum2}]\;\;\seq{Q\sred{\mu} Q'}{P+Q\sred{\mu}Q'}\\
\; &\;\\
\; [\mbox{\scriptsize Par1}]\;\;\seq{P\sred{\mu} P'}{P\mid Q\sred{\mu}P'\mid Q}
&
[\mbox{\scriptsize Par2}]\;\;\seq{Q\sred{\mu} Q'}{P\mid Q\sred{\mu}P\mid Q'}\\
\; &\;\\
\; [\mbox{\scriptsize Com}]\;\; \seq{P\sred{a} P'\quad Q\sred{\ol{a}}Q'}{P\mid Q\sred{\tau}P'\mid Q'}\quad&
\textcolor{violet}{[\mbox{\scriptsize Rec}]}\;\;
\textcolor{violet}{\seq{P[\vec{a}/\vec{x}]\sred{\mu} P' \quad \textcolor{darkgreen}{K(\vec{x}) \stackrel{def}{=} P \; \in \; D}}{K(\vec{a})\sred{\mu} P'}}
\end{array}
$$

\vskip 3mm
The reason for moving to ``modern'' CCS was to get static scope (thanks to the presence of the parameters). The old version had dynamic scope.  
}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Simulation and bisimulation}
\subsection{Simulation}
\begin{frame}
\frametitle{Simulation}
{\scriptsize
\begin{itemize}

\pause

\item {\bf Definition} We say that a relation {\cal R} on processes is a \textcolor{purple}{\em simulation} if
$$ P \;{\cal R}\; Q  \quad {\mbox{implies that}} \quad  \mbox{ {\it if} }  P\sred{\mu}P'  \mbox{ {\it then} } 
                                            \exists Q'   \mbox{ {\it s.t.} }   Q\sred{\mu}Q'  \mbox{ {\it and } }  P' \;{\cal R}\; Q'$$

\vskip 3mm
\pause
\item Note that this property does not uniquely defines $\cal R$. There may be several relations that satisfy it.

\vskip 3mm
\pause
\item Define $\lesssim \;\; = \;\; \bigcup \{ {\cal R} \;|\; {\cal R} \mbox{ is a simulation}\}$

\vskip 3mm
\pause
\item {\bf Theorem} $\lesssim$  is a bisimulation (\textcolor{darkgreen}{Proof: Exercise})

\vskip 3mm
\pause
\item $P \lesssim Q$  intuitively means that $Q$ can do everything that $P$ can do. \textcolor{purple}{$Q$ simulates $P$}.

\end{itemize}
}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Bisimulation}
\begin{frame}
\frametitle{Bisimulation}
{\scriptsize
\begin{itemize}

\pause

\item {\bf Definition} We say that a relation {\cal R} on processes is a \textcolor{purple}{\em bisimulation} if
$$ P \;{\cal R}\; Q  \quad {\mbox{implies that}} 
\begin{array}[t]{l}
\mbox{ {\it if} }  P\sred{\mu}P'  \mbox{ {\it then} } 
                                            \exists Q'   \mbox{ {\it s.t.} }   Q\sred{\mu}Q'  \mbox{ {\it and } }  P' \;{\cal R}\; Q'\\
\mbox{ {\it if} }  Q\sred{\mu}Q'  \mbox{ {\it then} } 
                                            \exists P'   \mbox{ {\it s.t.} }   P\sred{\mu}P'  \mbox{ {\it and } }  P' \;{\cal R}\; Q'
\end{array}
$$

\vskip 3mm
\pause

\item Again, this property does not uniquely defines $\cal R$. There may be several relations that satisfy it.
\vskip 3mm

\pause
\item Define $\sim \;\; = \;\; \bigcup \{ {\cal R} \;|\; {\cal R} \mbox{ is a bisimulation}\}$

\vskip 3mm

\pause
\item {\bf Theorem} $\sim$  is a bisimulation (\textcolor{darkgreen}{Proof: Exercise})

\vskip 3mm
\pause
\item $P \sim Q$  intuitively means that $Q$ can do everything that $P$ can do, and vice versa, at every step of the computation. 
\textcolor{purple}{$Q$ is bisimilar to $P$}.

\end{itemize}
}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Proof methods}
\begin{frame}
\frametitle{Proof methods}
\begin{itemize}
\pause
\item
Simulation and bisimulation are coinductive definitions. 
\vskip 3mm
\pause
\item In order to prove that $P\lesssim Q$ it is sufficient to find a simulation $\cal R$ such that 
  $P \;{\cal R}\; Q$

\vskip 3mm
\pause
\item Similarly, in order to prove that $P\sim Q$ it is sufficient to find a bisimulation $\cal R$ such that 
  $P \;{\cal R}\; Q$
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Examples and exercises}
\begin{frame}
\frametitle{Examples and exercises}
{\scriptsize
\begin{itemize}
\pause
\item 
Consider the following processes
\begin{itemize}
{\scriptsize
\item \textcolor{purple}{$P = a.(b.0 + c.0)$}
\item \textcolor{blue}{$Q = a.b.0 + a.c.0$}
}
\end{itemize}
Prove that $Q \lesssim P$ but $P \not \lesssim Q$ and $Q \not \sim P$

\pause
\vskip 3mm
\item 
Assume that  $Q \lesssim P$ and  $P \lesssim Q$ (for two generic $P$ and $Q$). Does it follow that $P\sim Q$? 

\pause
\vskip 3mm
\item 
Consider the following processes
\begin{itemize}
{\scriptsize
\item \textcolor{purple}{$R = a.(b.0 + b.0)$}
\item \textcolor{blue}{$S = a.b.0 + a.b.0$}
}
\end{itemize}
Prove that $Q \sim P$  


\pause
\vskip 3mm
\item Consider the two definitions of semaphore given at the beginning of this lecture. 
Prove that they are bisimilar.

\pause
\vskip 3mm
\item Consider the processes $H(a)$ and $K(a)$ defined by 
$H(x) \stackrel{def}{=} x.H(x) $ and $K(x) \stackrel{def}{=} x.K(x)\; |\; x.K(x) $. Are they bisimilar? 

\pause
\vskip 3mm
\item What is the smallest bisimulation? 

\end{itemize}
}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Alternative characterization of bisimulation}
\begin{frame}
\frametitle{Bisimulation as greatest fixpoint}
{\scriptsize
\begin{itemize}
\pause
\vskip 3mm
\item Consider the set of relations on processes  (that is, on the powerset of the cartesian product on processes) ordered by set inclusion. Obviously, this is a complete lattice.

\vskip 3mm
\item {\bf Definition} Let  $\cal F$ be a function on relation defined in the following way:   

$$ P \;{\cal F}({\cal R})\; Q  \quad {\mbox{iff}} 
\begin{array}[t]{l}
\mbox{ {\it if} }  P\sred{\mu}P'  \mbox{ {\it then} } 
                                            \exists Q'   \mbox{ {\it s.t.} }   Q\sred{\mu}Q'  \mbox{ {\it and } }  P' \;{\cal R}\; Q'\\
\mbox{ {\it if} }  Q\sred{\mu}Q'  \mbox{ {\it then} } 
                                            \exists P'   \mbox{ {\it s.t.} }   P\sred{\mu}P'  \mbox{ {\it and } }  P' \;{\cal R}\; Q'
\end{array}
$$
\pause
\vskip 3mm
\item {\bf Lemma} $\cal F$ is monotonic
\pause
\vskip 3mm
\item {\bf Theorem (Knaster-Tarski)}  {\cal F} has (unique) least and greatest fixpoints, and
$$\;{\it lfp}({\cal F}) \;=\; \bigcap \{{\cal R} \;|\; {\cal F}({\cal R}) \subseteq {\cal R}\}$$
$${\it gfp}({\cal F}) \;=\; \bigcup \{{\cal R} \;|\; {\cal R}\subseteq{\cal F}({\cal R})\}$$

\pause
\vskip 3mm
\item {\bf Corollary}  \ \ $\sim \;=\;{\it gfp}({\cal F})$

\pause
\vskip 3mm
\item A similar characterization, of course, holds for $\lesssim$ as well.
\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Bisimulation in CCS is a congruence}
\begin{frame}
\frametitle{Bisimulation in CCS is a congruence}
\begin{itemize}
\item {\bf Definition} A relation {\cal R} on a language is called \textcolor{purple}{\em congruence} if
\begin{itemize}
\item $\cal R$ is an equivalence relation (i.e. it is reflexive, symmetric, and transitive), and 
\item $\cal R$ is preserved by all the operators of the language, namely if $P\;{\cal R}\; Q$ then 
${\it op}(P,\vec{R}) \;{\cal R}\; {\it op}(P,\vec{R})$
\end{itemize}
\pause
\vskip 3mm
\item {\bf Theorem } $\sim$ is a congruence relation
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Exercises}
\begin{frame}
\frametitle{Exercises}
\begin{itemize}
\item Complete the proof that bisimulation in CCS is a congruence
\vskip 3mm
\item Prove that if $P \lesssim Q$ then the traces of $P$ are contained in the traces of $Q$
\vskip 3mm
\item Prove that if $P \sim Q$ then $P \lesssim Q$ and  $Q \lesssim P$
\vskip 3mm
\item Prove that 
\begin{itemize}
 \item $P + 0 \sim P$ and  $P | 0 \sim P$ 
 \item  $P + P \sim P$  but (in general)  $P | P \not \sim P$ 
 \item $P + Q  \sim Q + P$ and $P | Q  \sim Q | P$ 
 \item $(P + Q) + R \sim P + (Q + R) $ and  $(P | Q) | R \sim P | (Q | R) $
\end{itemize}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}



