\documentclass[compress]{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
\newcommand{\os}{[\![}
\newcommand{\cs}{]\!]}
\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 5] % (optional, use only with long paper titles)
{Concurrency 5}

\subtitle{CCS - Up-to bisimulation. Weak bisimulation. Axiomatizations. }

\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:
\AtBeginSection[]
{
  \begin{frame}<beamer>
    \frametitle{Outline}
    \tableofcontents[currentsection,currentsubsection]
  \end{frame}
}
\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{Outline}
  \tableofcontents
  % You might wish to add the option [pausesections]
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[Summary]{A brief summary of the main notions seen in previous lectures}
\subsection*{}
\begin{frame}
\frametitle{A brief summary: Syntax of CCS}
{\scriptsize
\begin{itemize}
\item \textcolor{purple}{(channel, port) names}: \; $a, b, c, \ldots$
\item \textcolor{purple}{co-names}: \; $\overline a, \overline b, \overline c, \ldots$  \qquad Note: \; $\overline{\overline a} = a$
\item \textcolor{purple}{silent action}: \; $\tau$
\vskip 3mm
\item \textcolor{purple}{actions, prefixes}: $\mu\; \mbox{::=}\;\; a\;\;|\;\;\overline 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}}\\
      & | &  { {K(\vec{a})}} &\mbox{\textcolor{darkgreen}{process name with parameters}}\\
\end{array}$
\vskip 3mm
\item   \textcolor{purple}{Process definitions:}
$\begin{array}[t]{lcll}
 D &\mbox{::=} &  {K(\vec{x}) \stackrel{\rm def}{=} P } & \textcolor{darkgreen}{\mbox{ where }{\it fn}(P) \subseteq \vec{x}}
\end{array}$
\vskip 3mm
\item  ${\it fn}(P)$ is the set of free (channel) names in $P$ (occurrences not in the scope of $\nu$)
\item  conversely, ${\it bn}(P)$ is the set of bound names in $P$ (occurrences in the scope of $\nu$)
\end{itemize}
}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{A brief summary: Labeled transition system for 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&
{[\mbox{\scriptsize Rec}]}\;\;
{\seq{P[\vec{a}/\vec{x}]\sred{\mu} P' \quad \textcolor{darkgreen}{K(\vec{x}) \stackrel{\rm def}{=} P \; \in \; D}}{K(\vec{a})\sred{\mu} P'}}
\end{array}
$$

}

\end{frame}

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

\begin{frame}
\frametitle{A brief summary: (Strong) Bisimulation and Bisimilarity}
{\scriptsize
\begin{itemize}



\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


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


\item {\bf Definition}\   \textcolor{purple}{(Bisimilarity)}\ 
 $\sim \;\; = \;\; \bigcup \{ {\cal R} \;|\; {\cal R} \mbox{ is a bisimulation}\}$

\vskip 3mm


\item {\bf Theorem} \ $\sim$  is a bisimulation.

\vskip 3mm

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

\end{itemize}
}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{A brief summary: The coinductive method}
\begin{itemize}

\item
Bisimilarity is a coinductive definition. 
\vskip 3mm

\item 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}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[Bisimilarity]{Properties of bisimilarity}
\subsection{Bisimilarity is a congruence}
\begin{frame}
\frametitle{Bisimilarity in CCS is a congruence}
\begin{itemize}
\item {\bf Definition} A relation $\textcolor{purple}{\cal R}$ on a language is a 
\textcolor{purple}{\em congruence} if
\begin{itemize}
\item $\textcolor{purple}{\cal R}$ is an equivalence relation (i.e. it is reflexive, symmetric, and transitive), and 
\item $\textcolor{purple}{\cal R}$ is preserved by all the operators of the language, namely if $\textcolor{blue}{P}\;\textcolor{purple}{\cal R}\; \textcolor{blue}{Q}$ then 
$\textcolor{darkgreen}{{\it op}(P_1,\ldots, \textcolor{blue}{P},\ldots, P_n) \;\textcolor{purple}{\cal R}\; {\it op}(P_1,\ldots, \textcolor{blue}{Q},\ldots, P_n)}
$
\end{itemize}

\vskip 3mm
\item {\bf Theorem } $\sim$ is a congruence relation
\vskip 3mm
\item This is an important property as it allows to prove equivalence in a modular way.
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Proof of the congruence theorem}
\begin{itemize}
\item Bisimilarity is an equivalence relation.
\begin{itemize}
\item \textcolor{purple}{Reflexivity}. Let ${\cal R} = \{ (P,P) \;|\; P \mbox{ is a CCS process }\}$. 
Then ${\cal R}$ is a bisimulation (Immediate).
\item \textcolor{purple}{Symmetry}. If  $ P\; {\cal R}\; Q $, with $ {\cal R} $ bisimulation, 
then $Q \;{\cal R}^{-1}\; P$ holds and $ {\cal R}^{-1} $ is a bisimulation (Immediate).
\item \textcolor{purple}{Transitivity}. If  $ P\; {\cal R}\; Q $ and $ Q\; {\cal S}\; R $, with $ {\cal R}, {\cal S} $ bisimulations, 
then $P\; {\cal R}\circ{\cal S}\; R$ holds and $ {\cal R}\circ{\cal S}$ is a bisimulation (Proof: exercise).
\end{itemize}
\vskip 3mm
\item We have to prove now that $\sim$ is preserved by the operators of CCS. We prove it for
the most complicated case, the parallel operator, and we leave the others as exercise. 
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Proof of the congruence theorem: case of the parallel operator}
{\scriptsize

Assume $P\sim Q$. We prove that for any $R$,  $P\;|\; R \sim Q \; | \; R$ holds.
 (The case $R\;|\; P \sim R \; | \; Q$ is analogous).
Let 
$${\cal R} = \{ (P'\; | \; R', Q'\; | \; R') \;|\; P', Q', R'
\mbox{ are CCS processes and $P'\sim Q'$ }\}$$
We only need to prove that  ${\cal R}$ is a bisimulation.


{\scriptsize
\begin{itemize}
\item \textcolor{purple}{(Decomposition phase)} Assume $P'\;|\;R'\sred{\mu}P''\;|\;R''$. There are 
three cases, corresponding to the three rules for parallel composition. 
\begin{itemize}
{\scriptsize
\item (Rule Par1) In this case $P'\sred{\mu}P''$ and $R''= R'$. Since 
$P' \sim Q'$, there exists $Q''$ such that $Q'\sred{\mu}Q''$ and $P'' \sim Q''$.
\item (Rule Par2) In this case $P''=P'$ and $R'\sred{\mu} R''$. Take $Q''= Q'$.
\item (Rule Com) In this case $P'\sred{a}P''$, $R'\sred{\overline a}R''$, and 
$\mu = \tau$. Since 
$P' \sim Q'$, there exists $Q''$ such that $Q'\sred{a}Q''$ and $P'' \sim Q''$.
}
\end{itemize}
\item \textcolor{purple}{(Composition phase)} In each of the three cases, 
$Q'\; | \; R' \sred{\mu}Q''\;|\;R''$ for some $Q''$ such that 
$P'' \sim Q''$, and therefore $P''\; | \; R''\; {\cal R}\; Q''\;|\;R''$ holds.

\end{itemize}
}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Some interesting bisimilarities}
\begin{frame}
\frametitle{Some interesting bisimilarities}
{\scriptsize The following bisimilarities hold

$$\begin{array}{rcllrcl}
P+0  &\sim &  P   &   \qquad &P\;|\; 0   &\sim   & P \\ 
P+Q  &\sim &  Q+P &   \qquad &P\;|\; Q   &\sim   & Q \;|\; P \\
(P+Q) + R  &\sim &  P + (Q+R) &   \qquad &(P\;|\; Q)\;| \;R   
                           &\sim   & Q \;|\; ( P\;|\; R)\\
P+P  &\sim &  P &
\end{array}
$$

$$ \begin{array}{rcll}
(\nu a) 0   &\sim &  0\\ 
(\nu a) (P\;|\;Q)   &\sim &  P \;|\;(\nu a)Q  &   \mbox{if $a\not\in {\it fn}(P)$}\\ 
(\nu a) (P+Q)   &\sim &  P + (\nu a)Q  &   \mbox{if $a\not\in {\it fn}(P)$}\\ 
(\nu a) (\nu b) P   &\sim &  (\nu b) (\nu a)P &   \\ 
(\nu a) (P)   &\sim &  (\nu b)P[b/a]  &   \mbox{if $a$ not in the scope of $(\nu b)$ in $P$ \textcolor{purple}{($\alpha$ conversion)}}\\ 
(\nu a) b.P   &\sim &  0  &   \mbox{if $b = a$ or  $b = \overline a$}\\ 
(\nu a) b.P   &\sim &  b.(\nu a) P  &   \mbox{if $b \neq a$ and  $b \neq \overline a$}\\
\; \\
K(\vec a) &\sim & P[\vec a / \vec x]&  \mbox{if }  K(\vec x) \stackrel{\rm def}{=} P
\end{array}
$$

Proof: Exercise
}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Some interesting bisimilarities: The Expansion Laws}
{\scriptsize The following bisimilarities hold

$$\begin{array}{rcll}
a.P \;|\; b.Q   &\sim &  a.(P \;|\;b.Q) \; + \; b.(a.P \;| \;Q)   \;  \mbox{  if } b\neq \overline a \\ 
a.P \;|\; \overline a.Q   &\sim &  a.(P \;|\;\overline a.Q) \; + \; \overline a.(a.P \;| \;Q) \; + \; \tau.(P\;|\;Q)\\ 
\;
\end{array}
$$

More in general:

$$ \begin{array}{rcl}
(P\;|\;Q)   &\sim & (\mu. \sum_{P \sred{\mu} P'} P'\;|\;Q) \;  + \;  (\mu. \sum_{Q \sred{\mu} Q'} P\;|\;Q') \; 
+ \;
(\tau.\sum_{\stackrel{P \sred{a} P'}{Q\sred{\overline a}Q'}} P'\;|\;Q')\\
\;
\end{array}
$$
Proof: Exercise
}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[Axiomatization]{Axiomatization of strong bisimilarity}
\subsection*{}
\begin{frame}
\frametitle{Axiomatization of strong bisimilarity}
{\scriptsize 
An equational theory for CCS: the axioms are the ``$=$'' version  of the bisimilarities seen in previous pages. 
That is: 

$$\begin{array}{rcllrcl}
P+0  &= &  P   &   \qquad &P\;|\; 0   &=   & P \\ 
P+Q  &= &  Q+P &   \qquad &P\;|\; Q   &=   & Q \;|\; P \\
(P+Q) + R  &= &  P + (Q+R) &   \qquad &(P\;|\; Q)\;| \;R   
                           &=   & Q \;|\; ( P\;|\; R)\\
P+P  &= &  P &
\end{array}
$$

$$ \begin{array}{rcll}
(\nu a) 0   &= &  0   &   \\ 
(\nu a) (P\;|\;Q)   &= &  P \;|\;(\nu a)Q  &   \mbox{if $a\not\in {\it fn}(P)$}\\ 
(\nu a) (P+Q)   &= &  P + (\nu a)Q  &   \mbox{if $a\not\in {\it fn}(P)$}\\ 
(\nu a) (\nu b) P   &= &  (\nu b) (\nu a)P &   \\ 
(\nu a) (P)   &= &  (\nu b)P[b/a]  &   \mbox{if $a$ not in the scope of $(\nu b)$ in $P$ \textcolor{purple}{($\alpha$ conversion)}}\\ 
(\nu a) b.P   &= &  0  &   \mbox{if $b = a$ or  $b = \overline a$}\\ 
(\nu a) b.P   &= &  b.(\nu a) P  &   \mbox{if $b \neq a$ and  $b \neq \overline a$}\\
\; \\
K(\vec a) &= & P[\vec a / \vec x]&  \mbox{if }  K(\vec x) \stackrel{\rm def}{=} P
\end{array}
$$

$$ \begin{array}{rcl}
(P\;|\;Q)   &= & (\mu. \sum_{P \sred{\mu} P'} P'\;|\;Q) \;  + \;  (\mu. \sum_{Q \sred{\mu} Q'} P\;|\;Q') \; 
+ \;
(\tau.\sum_{\stackrel{P \sred{a} P'}{Q\sred{\overline a}Q'}} P'\;|\;Q')
\end{array}
$$
}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Axiomatization of strong bisimilarity}
{\scriptsize 

To prove equivalence of recursive processes, it is convenient to introduce also the following conditional axiom 
(\textcolor{purple} {Unique solution of equations}):
\vskip 3mm
Given a context $C[\;]$ (that is, a term with some ``holes'' $[\;]$), in which  all 
the holes are guarded (that is, occur in the context of a prefix), then, for every $P$ and $Q$
$$ \mbox{if \ \  } P = C[P] \mbox{ \  \ and \ \ }  Q = C[Q] \mbox{ \ \ then \ \  }  P = Q$$

\vskip 3mm
{\bf Definition}\  \ We write \ \  ${\it Ax} \vdash P = Q$  \ iff \ $P = Q$ is derivable from the above axioms {\it Ax}
 and the usual rules for equality 

\vskip 3mm
{\bf Theorem}\ \ \textcolor{purple}{(Soundness of the axiomatization)}\  If \ ${\it Ax} \vdash P = Q$  \ then \ $P \sim Q$.

\vskip 3mm
The converse of the above theorem does not hold, i.e. the axiomatization is not complete. Note that the existence of
 a sound and complete 
axiomatization  would imply the
decidability of bisimilarity (because the complement of the bisimarity relation is semidecidable). However, bisimilarity is 
not decidable in CCS.

\vskip 3mm
The characterization of subsets of CCS in which bisimulation is decidable is an important research field in Concurrency Theory.

}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Bisimulation up-to $\sim$}
\subsection*{}
\begin{frame}
\frametitle{Bisimulation up-to $\sim$}
{\scriptsize
The axiomatization can be combined with the coinductive method to ease proving bisimilarity. The idea is based on the 
so-called ``bisimulation up-to $\sim$'' technique.
\vskip 3mm

\begin{itemize}
\item {\bf Definition} We say that a relation ${\cal R}$ on processes is a \textcolor{purple}{\em bisimulation up-to $\sim$} 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' \sim{\cal R}\sim 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' \sim{\cal R}\sim Q'
\end{array}
$$
Notation: $P' \sim{\cal R}\sim Q'$ means: $\exists P'', Q''$ s.t. $P' \sim P''$, $P''\;{\cal R}\;Q''$, and $Q''\sim Q'$.

Note that in order to prove 
$P' \sim P''$ and $Q''\sim Q'$, it is sufficient to prove ${\it Ax}\vdash P'= P''$ and ${\it Ax}\vdash Q''= Q'$ .

\item {\bf Theorem} \ If there exists $\cal R$ such that $\cal R$ is a  bisimulation up-to $\sim$, and 
$P \; {\cal R}\; Q$ holds, then  $P \sim Q$  holds.
\end{itemize}
\vskip 3mm

The advantage of the above technique is that it is usually easier to define a relation that is a 
bisimulation up-to $\sim$, rather than a bisimulation.

}
\end{frame}

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

\begin{frame}
\frametitle{Exercises}
\begin{itemize}
\item Prove that $A \sim B$ where $A \stackrel{\rm def}{=} a.A$ and $B \stackrel{\rm def}{=} a.B + a.a.B$
\vskip 3mm
\item Prove that the two definitions of semaphores given in previous lecture are equivalent (that is, the 
semaphores given by those two definitions  are bisimilar)
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Value-passing CCS}
\subsection*{}
\begin{frame}
\frametitle{Value-passing CCS}
{\scriptsize
In pure CCS processes communicate via channel (or port) names, 
but the communication does not carry data (or values). We now illustrate how we can modify 
CCS so that processes can send (and receive) values.

%\vskip 3mm
\begin{itemize}
\item \textcolor{purple}{(data) variables: \; $y, z, \ldots$}
\item \textcolor{purple}{(data) values: \; $v, w,  \ldots$}
%\vskip 3mm
\item {(channel, port) names}: \; $a, b, c, \ldots$
\item {co-names}: \; $\overline a, \overline b, \overline c, \ldots$
\item {silent action}: \; $\tau$
%\vskip 3mm
\item {actions, prefixes}: $\mu\; \mbox{::=}\;\; a\textcolor{purple}{\langle \vec y\rangle}\;\;|\;\;\overline {a}\textcolor{purple}{\langle \vec v\rangle} \;\;|\;\; \tau$ 
%\vskip 3mm
\item {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}}\\
      & | &  {K(\vec{a})} \textcolor{purple}{\langle \vec v\rangle} &\mbox{\textcolor{darkgreen}{process name with parameters}}\\
\end{array}$
%\vskip 3mm
\item   {Process definitions:}
$\begin{array}[t]{lcll}
 D &\mbox{::=} &  {K(\vec{x})\textcolor{purple}{\langle \vec y\rangle} \stackrel{\rm def}{=} P } & \textcolor{darkgreen}{\mbox{ where }{\it fn}(P) \subseteq \vec{x}}
\end{array}$
%\vskip 3mm
\end{itemize}
}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{The labeled transition system for value-passing CCS}
{\small We assume a given set of definitions $D$
\vskip 3mm

$$\begin{array}{cc}
\; [\mbox{\scriptsize \textcolor{purple}{Send}}] \;\; \frac{}{ \ol {a}\textcolor{purple}{\langle \vec v\rangle}.P\sred{a\textcolor{purple}{\langle \vec v\rangle}}P}\\
\; [\mbox{\scriptsize \textcolor{purple}{Receive}}] \;\; \frac{}{ a\textcolor{purple}{\langle \vec y\rangle}.P\sred{a\textcolor{purple}{\langle \vec v\rangle}}P\textcolor{purple}{[\vec v/\vec y]}}
 & [\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\textcolor{purple}{\langle \vec v\rangle}} P'\quad Q\sred{\ol{a}\textcolor{purple}{\langle \vec v\rangle}}Q'}{P\mid Q\sred{\tau}P'\mid Q'}\quad&
{[\mbox{\scriptsize Rec}]}\;\;
{\seq{P[\vec{a}/\vec{x}]\textcolor{purple}{[ \vec v/\vec y]}\sred{\mu} P' \quad \textcolor{darkgreen}{K(\vec{x})\textcolor{purple}{\langle \vec y\rangle} \stackrel{\rm def}{=} P \; \in \; D}}{K(\vec{a})\textcolor{purple}{\langle \vec v\rangle}\sred{\mu} P'}}
\end{array}
$$

Bisimulation and bisimilarity are defined as usual, considering as labels those of the form $a\textcolor{purple}{\langle \vec v\rangle}$ and $\overline{a}\textcolor{purple}{\langle \vec v\rangle}$
}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Translating value-passing CCS into pure CCS}
{\scriptsize 
If the domain $V$ of values is finite, we can emulate value-passing CCS by translating it into 
 pure CCS in the following way. We denote this translation by
$$[\![\cdot]\!] : \mbox{ value-passing CCS } \rightarrow \mbox{ pure CCS } $$
For simplicity we assume channel arity $1$.
\vskip 3mm
\renewcommand{\arraystretch}{1.5}
$$\begin{array}{rcl}
\os 0 \cs &=& 0 \\
\os \overline {a}\textcolor{purple}{\langle  v\rangle} . P \cs &=& \overline{a_{\textcolor{purple}{v}}} .\os  P \cs\\
\os  {a}\textcolor{purple}{\langle  y\rangle} . P \cs &=& \sum_{v\in V}a_{\textcolor{purple}{v}} .\os P\textcolor{purple}{[v/y]} \cs\\
\os P \,\mid\, Q \cs & = & \os P  \cs \,\mid\, \os Q \cs \\
\os P+Q \cs & = &  \os P \cs + \os Q \cs \\
\os (\nu a) P \cs & = & (\nu a) \os P \cs  \\
\os K(\vec{a})\textcolor{purple}{\langle  v\rangle} \cs & = & K_{\textcolor{purple}{v}} (\vec{a})\\
\end{array}$$
Furthermore, each definition ${K(\vec{x})\textcolor{purple}{\langle \vec y\rangle} \stackrel{\rm def}{=} P } $
is replaced by the following set of definitions, one for each $v\in V$:
$${K_{\textcolor{purple}{v}}(\vec{x}) \stackrel{\rm def}{=} [\![  P\textcolor{purple}{[v/y]} ]\!] } $$
\renewcommand{\arraystretch}{1}

}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section[Weak bisimilarity]{Weak Bisimilarity and Observation Congruence}
\subsection*{}
\begin{frame}
\frametitle{Weak Bisimulation and Weak Bisimilarity}
{\scriptsize 
Motivation: abstract from internal actions (i.e. $\tau$ actions)
\vskip 3mm
We introduce the following notation
\begin{itemize}
\item $P (\sred{\tau})^* Q$ \ \   iff \ \ $P = P_0 \sred{\tau} P_1 \sred{\tau} \ldots \sred{\tau} P_n =  Q$
\item $P \wred{\vec \mu} Q$ \ \  iff \\  $P = P_0 \; (\sred{\tau})^*\sred{\mu_1} (\sred{\tau})^*\; P_1 \; (\sred{\tau})^*\sred{\mu_2}(\sred{\tau})^* \ldots (\sred{\tau})^*\sred{\mu_n}(\sred{\tau})^* \; P_n =  Q$\ \  and \ \ ${\vec \mu}=\mu_1\mu_2\ldots\mu_n$
\item $P \wred{\widehat \mu} Q$ \ \  iff \\   $P \wred{\vec \mu} Q$ \ and \  ${\widehat \mu}$ \  is obtained from 
\ ${\vec \mu}$ \  by removing all the \  $\tau$'s
\end{itemize}
\vskip 6mm
Examples: \ \ $\widehat {a} = a$, \ \  $\widehat {\tau a \tau} = a$, \ \  $\widehat {\tau} = \varepsilon$ (empty string), \  \ 
$\widehat {a \tau b} = a b$.
\vskip 3mm
Note:
\begin{itemize}
 {\scriptsize
 \item $P \wred{\widehat {a}}  Q$ \ \  means \ \ $P\;\; (\sred{\tau})^*\sred{a} (\sred{\tau})^*\;\; Q$,
 \item $P \wred{\widehat {\tau}}  Q$ \ \  means \ \ $P \wred{\varepsilon} Q$, \ \ namely \ \  $P\;\; (\sred{\tau})^*\;\; Q$,
 \item $P \wred{\tau}  Q$ \ \ means \ \ $P\;\; (\sred{\tau})^*\sred{\tau} (\sred{\tau})^* \;\; Q$, \ \ namely \ \ $P \;\; (\sred{\tau})^+ \;\; Q$ \ \ (at least one $\tau$-step).
 }
\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Weak Bisimulation and Weak Bisimilarity}
{\scriptsize 
\begin{itemize}
\item {\bf Definition} \ We say that a relation {\cal R} on processes is a \ \textcolor{purple}{\em weak 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\wred{\widehat \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\wred{\widehat \mu}P'  \mbox{ {\it and } }  P' \;{\cal R}\; Q'
\end{array}
$$

\vskip 3mm


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


\item {\bf Definition}\ \  \textcolor{purple}{(Bisimilarity)} \ \ $\approx \;\; = \;\; \bigcup \{ {\cal R} \;|\; {\cal R} \mbox{ is a weak bisimulation}\}$

\vskip 3mm


\item {\bf Theorem} \ \ $\approx$ \  is a weak bisimulation.

\vskip 3mm

\item $P \approx Q$ \ \textcolor{purple}{($P$ is weakly bisimilar to $Q$)} \ 
intuitively means that at every step of the computation $Q$ can do everything that $P$ can do, and vice versa, if we ignore the internal actions. 

\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Observation congruence}
{\scriptsize 
Unfortunately $\approx$ is not a congruence.\\ 
Example: 
$a.P \approx \tau.a.P$ but $a.P + b.Q \not \approx \tau.a.P + b.Q$ 
\vskip 3mm
\begin{itemize}
\item {\bf Definition} We say that $P$ and $Q$ are \ \textcolor{purple}{\em observation-congruent} \ 
(notation $P \cong Q$) iff 
$$
\begin{array}[t]{l}
\mbox{ {\it if} }  P\sred{\mu}P'  \mbox{ {\it then} } 
                                            \exists Q'   \mbox{ {\it s.t.} }   Q\wred{\mu}Q'  \mbox{ {\it and } }  P' \approx Q'\\
\mbox{ {\it if} }  Q\sred{\mu}Q'  \mbox{ {\it then} } 
                                            \exists P'   \mbox{ {\it s.t.} }   P\wred{\mu}P'  \mbox{ {\it and } }  P' \approx Q'
\end{array}
$$

The difference between $\approx$ and $\cong$ is when the first step is a $\tau$-step. 
If $ P\sred{\tau}P'$ and $P\approx Q$, then we can take $Q' = Q$ provided that $P' \approx Q'$. On the contrary, if
$P\cong Q$, then we are obliged to find a $Q'$ such that $Q\wred{\tau}Q' $ 
(which means, at least one $\tau$-step from $Q$ to $Q'$), 
and $P' \approx Q'$.
\vskip 3mm

\item {\bf Theorem} \ \ $\sim \;\; \subseteq \;\; \cong \;\; \subseteq \;\; \approx $  
\vskip 3mm

Proof: exercise.

\vskip 3mm

\item {\bf Theorem}\ \  $\cong$ \  is a congruence, and more precisely, it 
is the largest congruence on CCS contained in $\approx$.

\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Properties of observation congruence}
\begin{frame}
\frametitle{Properties of observation congruence}
{\scriptsize 


{\bf Proposition } \ The following properties hold:
$$
\begin{array}{rcl}
 \mu.\tau.P &\cong& \mu.P\\
 P + \tau.P &\cong& \tau.P\\
\mu.(P + \tau.Q) + \mu.Q &\cong& \mu.(P + \tau.Q)
\end{array}
$$

Proof: exercise.
\vskip 3mm
The above properties are used to give an axiomatization observation congruence. The ``='' version of the above are called  
\textcolor{purple}{$\tau$-laws}:
$$
\begin{array}[t]{rcl}
 \mu.\tau.P &=& \mu.P\\
 P + \tau.P &=& \tau.P\\
\mu.(P + \tau.Q) + \mu.Q &=& \mu.(P + \tau.Q)
\end{array}
$$

{\bf Definition } \ We write \ ${\it Ax}_\tau \vdash P = Q$ \ iff \ $P=Q$ can be derived from the 
axioms {\it Ax}, the $\tau$-laws, and the usual rules for equality. 

\vskip 3mm

{\bf Theorem } \ (Soundness) \ If ${\it Ax}_\tau \vdash P = Q$ \ then \ $P \cong Q$.

}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Properties of observation congruence}
{\scriptsize 
The following properties that can be useful to 
prove observation congruence
\begin{itemize}
\item If \ $P\approx Q$ \ \   then \ \ $\mu.P \cong \mu.Q$
\item  $P\approx Q$ \ \ \   iff  \ \ \  $P \cong Q$ \ or \  $P \cong \tau.Q$ \ or \  $\tau.P \cong Q$ 
\end{itemize}

\vskip 3mm

Exercise: 
\begin{itemize}
\item Assume \ \  $A \stackrel{\rm def}{=} a.b.0 + a.c.0$ \ \  and \ \ 
$B  \stackrel{\rm def}{=} a.(\tau.b.0 + \tau.c.0)$. \ \ Prove that  $A \cong B$.
\item Assume \ \ $A \stackrel{\rm def}{=} (\nu b) (a.b.c.0 + a.{\bar b}.c.0)$ 
\ \ and \  \ 
$B  \stackrel{\rm def}{=} a.a.c.c.0$. \ \ 
Prove that  $A \cong B$.
\end{itemize}

}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Example: FIFO Queues}
\begin{frame}
\frametitle{Two equivalent definitions of FIFO Queues}
{\scriptsize 
Consider the following definitions of a FIFO queue with 2 positions in value-passing CCS
\vskip 3mm
\begin{block}{First definition}
$\begin{array}{rcl}
Q_{2}({\it in}, {\it out}) &\stackrel{\rm def}{=}& {\it in}(y).Q_{1}({\it in},{\it out})\langle y\rangle\\
Q_{1}({\it in}, {\it out}) \langle y\rangle &\stackrel{\rm def}{=}& {\it in}(z).Q_{0}({\it in}, {\it out}) \langle z,y\rangle \;\; + \;\; \overline{{\it out}}\langle y\rangle. Q_{2}({\it in}, {\it out}) \\
Q_{0}({\it in}, {\it out}) \langle z,y\rangle &\stackrel{\rm def}{=}& \overline{{\it out}}\langle y\rangle.Q_{1}({\it in}, {\it out}) \langle z\rangle 
\end{array}$
\end{block}

\begin{block}{Second definition}
Here we define a 2-positions queue as the concatenation of two 1-position buffers
$\begin{array}{rcl}
B({\it in}, {\it out})  &\stackrel{\rm def}{=}& {\it in}(y).B'({\it in}, {\it out}) \langle y\rangle\\
B'({\it in}, {\it out}) \langle y\rangle &\stackrel{\rm def}{=}& \overline{{\it out}}\langle y\rangle.B({\it in}, {\it out})  \\
{\it Queue} ({\it in}, {\it out}) & \stackrel{\rm def}{=}& (\nu c) (B({\it in}, c) \;|\; B(c, {\it out}))
\end{array}$
\end{block}

\vskip 3mm

{\bf Exercise} \ Prove that $Q_{2}({\it in}, {\it out})$ is observation-congruent to ${\it Queue}({\it in}, {\it out})$. 

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

 \textcolor{purple}{($\tau$-laws)}

