\documentclass[11pt]{article}

\usepackage{amsmath}
\usepackage{array}

\usepackage{geometry}
\usepackage{fancyhdr}

\geometry{
  dvips,  
  a4paper,
  left=20mm, right=20mm,
  top=10mm, bottom=10mm,
  headheight=10mm, headsep=10mm,
  footskip=10mm
}

\renewcommand{\headrulewidth}{.1mm}
\renewcommand{\footrulewidth}{0mm}
\lhead{}
\chead{Concurrency problems class}
\rhead{\thepage}
\lfoot{}
\cfoot{}
\rfoot{}
\pagestyle{fancy}
\setlength{\parskip}{1pt}

%%% text macros
\newcommand{\pic}{$\pi$-calculus}
%%% end of text macros

%%% syntactic macros
\newcommand{\hide}[2]{(\nu\, #1)#2}  % e.g. \hide{L}{P}
\newcommand{\repl}[1]{\text{!}#1}  % e.g. \repl{P}
\newcommand{\relabel}[2]{#2[#1]}  % e.g. \relabel{f}{P}
\newcommand{\fixp}[2]{\mu #1. #2}  % e.g. \fixp{X}{P}
%%% end of syntactic macros

%%% math macros
\newcommand{\ar}[1]{\overset{#1}{\longrightarrow}} % e.g. \ar{a}
\newcommand{\infer}[2]{\frac{\displaystyle #1}{\displaystyle #2}}
\newcommand{\defeq}{\mathrel{\overset{\text{def}}{=}}}
\newcommand{\id}[1]{\mathit{#1}} % multi-letter identifiers
\newcommand{\RR}{\cal{R}}
\newcommand{\strongbisim}{\sim}
\newcommand{\weakbisim}{\approx}
\newcommand{\obscong}{\cong}
\renewcommand{\bar}{\overline}
%%% end of math macros

\begin{document}
\thispagestyle{empty}

\begin{center}
  {\Large Concurrency problems class}

  \bigskip

  Catuscia Palamidessi, Jean-Jacques L\'evy, James J. Leifer

  \medskip

  Catuscia@lix.polytechnique.fr, Jean-Jacques.Levy@inria.fr,
  James.Leifer@inria.fr

  \bigskip

  11 December 2003
\end{center}

\pagestyle{fancy}

\section{Definition: CCS processes}

\begin{center}
  \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
    P ::= {}
    &  0 & empty \\
    &  \alpha.P & prefixing \\
    &  P|P & parallel composition \\
    &  \hide{L}{P} & hiding \\
    &  P + P & summation \\
    \multicolumn{3}{l}{\dotfill} \\
    & K & constant (for expressing recursion) \\
    & \repl{P} & \pic{}-style replication (for expressing
    recursion) \\
    & \fixp{X}{P} & fixed-point (for expressing recursion) \\
%    & \relabel{f}{P} & relabelling \\
  \end{tabular}
\end{center}

\section{Definition: CCS alphabetic conventions}
                                %
\begin{center}
  \begin{tabular}{>{$}l<{$}l}
    a       & name \\
    \bar{a} & co-name \\
    \ell    & label (ranges over names and co-names) \\
    L       & label set \\
    f       & label map \\
    \alpha  & action (ranges over labels and $\tau$) \\
  \end{tabular}
\end{center}

\section{Definition: CCS labelled transitions rules}

\begin{itemize}

\item input: $a.P \ar{a} P$
  
\item output: $\bar{a}.P \ar{\bar{a}} P$
  
\item synchronization:
  $\infer{P \ar{\ell} P' \qquad Q \ar{\bar{\ell}} Q'}%
  {P | Q \ar{\tau} P' | Q'}$

\item choice:
  $\infer{P \ar{\alpha} P'}%
  {P + Q \ar{\alpha} P'}$ (and symmetrically)

\item parallel composition:
  $\infer{P \ar{\alpha} P'}%
  {P | Q \ar{\alpha} P' | Q}$ (and symmetrically)

\item hiding:
  $\infer{P \ar{\alpha} P'}%
  {\hide{L}{P} \ar{\alpha} \hide{L}{P'}}$ if $\alpha,\bar{\alpha}
  \notin L$

\item and others, for example...

\item constant:
  $\infer{P \ar{\alpha} P'}%
  {K \ar{\alpha} P'}$ if $K = P$

\item replication (many possible):
  $\infer{P | \repl{P} \ar{\alpha} P'}%
  {\repl{P} \ar{\alpha} P'}$

\item fixed-point (many possible):
  $\infer{P\{\fixp{X}{P}/X\} \ar{\alpha} P'}%
  {\fixp{X}{P} \ar{\alpha} P'}$  

% \item relabelling:
%   $\infer{P \ar{\alpha} P'}%
%   {\relabel{f}{P} \ar{f(\alpha)} \relabel{f}{P'}}$  

\end{itemize}

\section{Definition: CCS operational equivalences}

\begin{itemize}
\item strong simulation: a relation $\RR$ is a strong simulation if
  for all $(P,Q) \in \RR$ and $P \ar{\alpha} P'$, there exists $Q'$
  such that $Q \ar{\alpha} Q'$ and $(P',Q') \in \RR$.
  
\item strong bisimulation: a relation $\RR$ is a strong bisimulation
  if it and its inverse are strong simulations.
  
\item strong bisimilarity: $\strongbisim$ is the largest strong
  bisimulation.
  
\item weak simulation: a relation $\RR$ is a weak simulation if for
  all $(P,Q) \in \RR$ we have:

  \begin{enumerate}
  \item if $P \ar{\tau} P'$ then there exists $Q'$ such that $Q
    \ar{\tau}^{*} Q'$ and $(P',Q') \in \RR$.
  \item if $P \ar{\ell} P'$ then there exists $Q'$ such that $Q
    \ar{\tau}^{*}\ar{\ell}\ar{\tau}^{*} Q'$ and $(P',Q') \in \RR$.
  \end{enumerate}

\item weak bisimulation:  a relation $\RR$ is a weak bisimulation
  if it and its inverse are weak simulations.
  
\item weak bisimilarity (also known as bisimilarity, also known as
  observational equivalence): $\weakbisim$ is the largest weak
  bisimulation.
  
\item observational congruence: $\obscong$ is the largest symmetric
  relation satisfying the following property: if $P \obscong Q$ and $P
  \ar{\alpha} P'$ then there exists $Q'$ such that $Q \ar{\tau}^{*}\ar{\ell}\ar{\alpha}^{*} Q'$
  and $P' \weakbisim Q'$.
\end{itemize}

\section{Exercise (CCS): unreliable transmission medium}

A transmitter $T$, an unrealiable transmission medium $M$, and a
receiver $R$ are modelled as follows:
                                %
\[\begin{array}{l!{{}\defeq{}}l}
  T & \id{in}.\bar{i}.T' \\
  T' & r.\bar{i}.T' + a.T \\
  M & i.M' \\
  M' & \bar{o}.M + \tau.\bar{r}.M \\
  R & o.\bar{out}.\bar{a}.R
\end{array}\]

$M$ is an unreliable medium: having received an input message from $T$
(action $i$) it either outputs the message to $R$ (action $\bar{o}$),
or loses it (action $\tau$) and then sends a request for
retransmission (action $\bar{r}$).  If $R$ does receive the message,
it delivers it (action $\bar{\id{out}}$) and sends an acknowledgement
directly to $T$ (action $\bar{a}$).

\def\fancybuffer{$\hide{i,o,r,a}{(T|M|R)}$}
\begin{enumerate}
\item Calculate the transition graph of \fancybuffer{} and hence show
  that this process is observationally equivalent to a simple reliable
  buffer $B$ defined by:
                                %
  \[B \defeq \id{in}.\bar{\id{out}}.B\]

  \item Are \fancybuffer{} and $B$ observationally congruent?
    
  \item Do the two have the same behavior with respect to
    \emph{divergence}, that is can either perform a series of actions
    ending in an infinite sequence of $\tau$ actions?
\end{enumerate}

\section{Exercise (CCS): semaphores}

\begin{enumerate}
\item A \emph{semaphore} is a mechanism to prevent more than a certain
  number $n$ of clients from simultaneously entering their
  \emph{critical sections} to access a precious resource.  A client
  ``brackets'' its critical section by requesting entry permission
  (action $\bar{\id{wait}}$) and then signaling when it is finished
  (action $\bar{\id{signal}}$):
                                %
  \[ \bar{\id{wait}}
  \quad \text{...critical section...} \quad
  \bar{\id{signal}} \]
                                %
  Note that a mutual exclusion lock (mutex) is a special case (when
  $n=1$) of a semaphore.
  
  Define a CCS process to model a semaphore of capacity $n$.  Hint:
  create a constant $\id{Sem}^n_k$, for $0 < n$ and $0 \leq k \leq n$,
  that represent a semaphore in the state when $k$ clients are in their
  critical sections.  You will need to treat the cases $k=0$ and $k=n$
  specially.

% \item MAYBE CUT OUT... Does this semaphore protect against
%   \emph{starvation}?  In other words, is it possible for the semaphore
%   to be less than full an infinite number of times and yet always deny
%   a waiting client the right to enter?

% \item In the \pic we can design a variant of this semaphore that 
  
\end{enumerate}

\section{Exercise (CCS): deadlock}

We say that a process \emph{can deadlock} if it can perform a
sequence of actions to enter a state that is observationally
congruent ($\obscong$) to $0$.

Let
                                %
\[\begin{array}{l!{{}\defeq{}}l}
  C & g_0 . g_1 . p_0 . p_1 . C \\
  D & g_1 . g_0 . p_1 . p_0 . D \\
  S_0 & \bar{g_0} . \bar{p_0} . S_0 \\
  S_1 & \bar{g_1} . \bar{p_1} . S_1 \\
\end{array}\]

\begin{enumerate}
  \item For each of the following processes, determine whether or not
  it can deadlock:

  \[ \hide{g_0, p_0, g_1, p_1}{(C | C | S_0 | S_1)} \]
  \[ \hide{g_0, p_0, g_1, p_1}{(C | D | S_0 | S_1)} \]

  \item Prove that $P \obscong 0$ iff $P$ can do no action.

  \item Prove that $T \weakbisim 0$ where $T \defeq \tau.T$.

  \item Hence show that it is possible for a process that can deadlock
  to be observationally congruent to one that cannot deadlock.

\end{enumerate}
% \section{Exercise (CCS): alternating bit protocol}

% MAYBE DO

\section{Exercise (\pic): arithmetic}

We can define a process $N_n$ for representing the natural number $n$
as follows:
%
\[\begin{array}{l!{{}\defeq{}}l}
N_0(s,z) & \bar{z} \\
N_{n+1}(s,z) & \bar{s}.N_{n}(s,z)
\end{array}\]
%
Thus $N_n(s,z)$ ouputs $n$ times on $s$ and then outputs on $z$.

Our goal is define a process $A(s_0,z_0,s_1,z_1,s,z)$ for adding
numbers which has the property that
%
\[\hide{s_0,z_0,s_1,z_1}{(N_{n_0}(s_0,z_0) | N_{n_1}(s_1,z_1) |
  A(s_0,z_0,s_1,z_1,s,z))} \weakbisim N_{n_0+n_1}(s,z) \tag{*}\]
%
\begin{itemize}
\item First define a processes $C(s,z,s',z')$ for copying a number from
  $(s,z)$ to $(s',z')$ and prove that \[\hide{s,z}{(N_n(s,z) |
    C(s,z,s',z'))} \weakbisim N_n(s',z')\]
  
% \item Define a process $S(s,z,s',z')$ for calculating the successor of
%   a number and prove that \[\hide{s,z}{(N_n(s,z) | S(s,z,s',z'))}
%   \weakbisim N_{n+1}(s',z')\]

\item Then define addition $A(s_0,z_0,s_1,z_1,s,z)$ and prove
  $(*)$ above.
\end{itemize}
\end{document}

