\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 3] % (optional, use only with long paper titles)
{Concurrency 3}

\subtitle{CCS - Syntax and transitions, Equivalences}

\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{Outline}
  \tableofcontents
  % You might wish to add the option [pausesections]
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
\subsection{Motivations}
\begin{frame}
\frametitle{Why a Calculus for Concurrency?}

\begin{itemize}
\item The \textcolor{purple}{\emph{Calculus for Communicating Systems} (CCS)} was developed by R. Milner around the 80's.
\item Other Process Calculi were proposed at about the same time: the \emph{\textcolor{purple}{Theory of Communicating Sequential Processes}} by T. Hoare and the \emph{\textcolor{purple}{Algebra of Communicating Processes}}   ~~by J. Bergstra and J.W. Klop.

\item Researchers were looking for a calculus with few, orthogonal mechanisms, able to represent all the relevant concepts of concurrent computations. More complex mechanisms should be built by using the basic ones.

\begin{itemize}
\item To help understanding / reasoning about / developing formal tools for concurrency.
\item To play a role, for concurrency, like that of the $\lambda$-calculus for sequential computation. 
\end{itemize}
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Inadequacy of standard models of computations}
The $\lambda$ calculus, the Turing machines, etc. are computationally complete, yet do not capture the features of concurrent computations like
\begin{itemize}
\item Interaction and communication
\item Inadequacy of functional denotation
\item Nondeterminism
\end{itemize}

Note: nondeterminism in concurrency is different from the nondeterminism used in Formal Languages, like for instance the Nondeterministic Turing Machines. 
 
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{A few words about nondeterminism}

\begin{columns}
\begin{column}{5cm}
\begin{block}<1->{}{In standard computation theory, if we want to compute the partial function $f$ s.t. $f(0) = 1$, a Turing Machine like this one is considered ok}
\end{block}
\begin{block}<2->{}{
However, we would not be happy with a coffee machine that behaves in the same way}
\end{block}
\end{column}
\begin{column}{.5cm}
\ 
\end{column}
\begin{column}{5cm}
\includegraphics<1->[height=3cm]{fig/TM.pdf}
\\ \ \\
\includegraphics<2->[height=3cm]{fig/CM.pdf}
\end{column}
\end{columns}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Nondeterminism in sequential models}
\begin{itemize}
\item
Convenient tool for solving certain problems in an easy way or for characterizing complexity classes 
(examples: search for a path in a graph, search for a proof etc.) 
\vskip 3mm
\pause
\item Examples of nondeterministic formalisms:
{\footnotesize\begin{itemize}
\pause
\item The nondeterminismistic Turing machines
\pause
\item Logic languages like Prolog and $\lambda$ Prolog 
\end{itemize}
}
\vskip 3mm
\pause
\item The characteristics of nondeterminism in this setting:
{\footnotesize
\begin{itemize}
\pause
\item It can be eliminated without loss of computational power by using \textcolor{violet}{backtracking}.
\pause
\item \textcolor{purple}{Failures don't matter}: all what we are interested on is the existence of succesful computations. A failure is reported only if all possible alternatives fail. 
\end{itemize}
}
\end{itemize}


\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Nondeterminism in concurrent models}
{\small
\begin{itemize}
\item Nondeterminism may arise because of interaction between processes.
\vskip 3mm
\pause
\item The characteristics of nondeterminism in this setting:
{\footnotesize
\begin{itemize}
\pause
\item \textcolor{violet}{It cannot be avoided}. At least, not without loosing essential parts of expressive power. All interesting models of concurrency cope with nondeterminism.
\pause
\item  \textcolor{purple}{Failures do matter}. Chosing the wrong branch might bring to an "undesirable situation". Backtracking is usually not applicable (or very costly), because the control is distributed: we should restart not one but several processes. 
\end{itemize}
}
\pause
\item Hence controlling nondeterminism is very important. In sequential programming is just a matter of efficiency, here is a matter of avoiding getting stuck in a wrong situation.
\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Principles in CCS design}
\begin{frame}
\frametitle{The basic kind of interaction (1/2)}
{\small 
\begin{itemize}
\item A calculus should contain only the primary constructs. For instance, the primary form of interaction. \textcolor{purple}{\em But what is the primary form of interaction?}
\vskip 3mm 
\pause
\item
In general, concurrent languages can offer various kinds of communication. For instance:
{\footnotesize
\begin{itemize}
\pause 
\item Communications via shared memory.
\pause
\item Communication via channels.
\pause
\item Communication via broadcasting.
\end{itemize}
}
\item and we could make even more distinctions
{\footnotesize
\begin{itemize}
\pause
\item one-to-one / one-to-many
\pause
\item Ordered / unordered (i.e. queues / bags)
\pause
\item Bounded / unbounded. 
\end{itemize}
}
\pause
\vskip 3mm 
\item So what is the basic kind of communication? 
\pause
\item
For CCS the answer was:  ~\textcolor{purple}{\em none of the above!}

\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{The basic kind of interaction (2/2)}
{\footnotesize
\begin{itemize}
\item 
In CCS, the fundamental model of interaction is \textcolor{purple}{\em synchronous} and \textcolor{purple}{\em symmetric}, i.e. the partners act at the same time performing complementary actions. 
\pause
\item
This kind of interaction is called \textcolor{violet}{\em handshaking}: the partners agree simoultaneously on performing the two (complementary) actions.
\vskip 3mm
\pause
\item
In Java there is a separation between active objects (threads) and passive objects (resources). CCS avoids this separation: Every (non-elementary) entity is a process.
\pause
\item
For instance, consider two proceesses $P$ and $Q$ communicating via a buffer $B$. in CCS also $B$ is a process and the communication is between $P$ and $B$, and between $Q$ and $B$. 
\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example:  $P$ and $Q$ communicating via a buffer $B$}
\begin{center}\includegraphics[height=6cm]{fig/buffer.pdf}\end{center}
\vskip 3mm
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Syntax and Operational Semantics of CCS}
\subsection{Syntax}
\begin{frame}
\frametitle{Syntax of CCS}
{\footnotesize
\begin{itemize}
\pause
\item \textcolor{purple}{(channel, port) names}: \; $a, b, c, \ldots$
\pause
\item \textcolor{purple}{co-names}: \; $\bar a, \bar b, \bar c, \ldots$  \qquad Note: \; $\bar{\bar a} = a$
\pause
\item \textcolor{purple}{silent action}: \; $\tau$
\pause
\vskip 3mm
\item \textcolor{purple}{actions, prefixes}: $\mu\; \mbox{::=}\;\; a\;\;|\;\;\bar a \;\;|\;\; \tau$ 
\vskip 3mm
\pause
\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}}\\
      & | &  \REC_{K} P  &\mbox{\textcolor{darkgreen}{process $P$ with definition $K=P$}}\\
      & | &  {K} &\mbox{\textcolor{darkgreen}{(defined) process name}}\\
\end{array}$
\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Labeled transition System}
\begin{frame}
\frametitle{Labeled transition system}
\begin{itemize}
\item The semantics of CCS is defined by in terms of a 
\textcolor{purple}{\em labeled transition system}, which is a set of triples of the form
$$
P \sred{\mu} Q
$$
Meaning: \textcolor{darkgreen}{\em $P$ evolves into $Q$ \; by making the action $\mu$}. 

\vskip 3mm
\item The presence of the label $\mu$ allows us to keep track of the 
interaction capabilities with the environment.  

\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Structural operational semantics}
The transitions of CCS are defined by a set of inductive rules. 
The system is also called  \textcolor{purple}{\em structural semantics}
because the evolution of a process is defined in terms of the evolution of its components.
\pause

$$\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[{\sf rec}_K P/K]\sred{\mu} P'}
{{\sf rec}_K P\sred{\mu} P'}
\end{array}
$$
\end{frame}

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

\begin{frame}
\frametitle{Some examples}
\begin{columns}
\begin{column}{8cm}
\includegraphics[width=8cm]{fig/tree1.pdf}
\end{column}
\begin{column}{3cm}
\pause
\begin{block}{}{\scriptsize The restriction can be used to enforce synchronization}\end{block}
\pause
\begin{block}{}{\scriptsize The parallel operator may cause infinitely many different states}\end{block}
\pause
\begin{block}{}{\scriptsize The fragment of the calculus without parallel operator generates only finite automata / regular trees}\end{block}
\end{column}
\end{columns}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{What equivalence for CCS?}
\begin{frame}
\frametitle{Motivation}
\begin{itemize}
\pause
\item
It is important to define formally when two system can be considered equivalent
\vskip 3mm
\pause
\item There may be various "interesting" notion of equivalence, it depends on what we want (which observables we want to preserve)
\vskip 3mm
\pause
\item A good notion of equivalence should be a congruence, so to allow modular verification
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Examples: possible definitions of a coffee machine}
{\small
\begin{itemize}
\pause
\item $\REC_K {\it coin}.({\it coffee}.\ol{\it ccup}.K +
{\it tea}.\ol{\it tcup}.K)$
\pause
\vskip 3mm
\item  {\it coin}.$\REC_K ({\it coffee}.\ol{\it ccup}.{\it coin}.K +
{\it tea}.\ol{\it tcup}.{\it coin}.K)$
\pause
\vskip 3mm
\item  $\REC_K ({\it coin}.{\it coffee}.\ol{\it ccup}.K +
{\it coin}.{\it tea}.\ol{\it tcup}.K)$
\vskip 3mm
\pause 
\item \textcolor{purple}{Question: which of these machines can we safely consider equivalent?}
\vskip 3mm
\pause 
\item Note that these machines have all the same traces.
\end{itemize}
}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Exercises}
\begin{itemize}
\item Define in CCS a semaphore with initial value $n$
\item Show that maximal trace equivalence is not a congruence in CCS. By 
maximal traces here we mean the  traces of all possible (finite or infinite) maximal runs.
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}



