\documentclass{beamer}

\setbeamertemplate{footline}
{
\begin{beamercolorbox}{section in foot}
\vskip-2mm \hskip 2mm\insertpagenumber
\end{beamercolorbox}
}

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


% 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}



