\documentclass[11pt]{article}
%\usepackage{times}
\usepackage{amsmath}
\usepackage{array}

\usepackage{geometry}
\usepackage{fancyhdr}

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

\renewcommand{\headrulewidth}{.1mm}
\renewcommand{\footrulewidth}{0mm}
\lhead{}
\chead{Midterm 2005 solutions}
\rhead{\thepage}
\lfoot{}
\cfoot{}
\rfoot{}
\pagestyle{fancy}
\setlength{\parskip}{1pt}

\newif\ifslidegeometry
\slidegeometryfalse
\input{../../../pi/common.tex}

\usepackage{color}
\usepackage{graphicx}
\newcommand{\dotdia}[1]{\begingroup\input{#1.tex}\input{#1.pstex_t}\endgroup}

\begin{document}

\begin{center}
\large
MPRI Concurrency (Cours 2-3) \\
Midterm Exam Solutions, 2005-2006 \\
25 Jan 2006 \\
James.Leifer@inria.fr \\
\end{center}

\section*{Quick review of CCS operational equivalences}

\begin{description}
\item[Strong simulation:] a relation $\RR$ is a strong simulation if
  for all $(P,Q) \in \RR$ and $P \red{\alpha} P'$, there exists $Q'$
  such that $Q \red{\alpha} Q'$ and $(P',Q') \in \RR$.
  
\item[Strong bisimilarity:] $\ccsstrongbisim$ 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 \red{\tau} P'$ then there exists $Q'$ such that $Q
    \redstar{\tau} Q'$ and $(P',Q') \in \RR$.
  \item if $P \red{\alpha} P'$ and $\alpha\neq\tau$ then there exists $Q'$ such that $Q
    \redstar{\tau}\red{\alpha}\redstar{\tau} Q'$ and $(P',Q') \in \RR$.
  \end{enumerate}

\item[Weak bisimilarity] (also known as bisimilarity, also known as
  observational equivalence): $\ccsweakbisim$ is the largest weak
  bisimulation.
  
\item[Observational congruence:] $\ccsobscong$ is the largest symmetric
  relation satisfying the following property: if $P \ccsobscong Q$
  and $P  \red{\alpha} P'$ then there exists $Q'$ such that $Q
  \redstar{\tau}\red{\alpha}\redstar{\tau} Q'$ and $P' \ccsweakbisim Q'$.
\end{description}

Note that $(\ccsstrongbisim) \subseteq (\ccsobscong) \subseteq
(\ccsweakbisim)$. We will freely use these inclusions throughout.

\section*{Question 1}

\begin{enumerate}
\item We show that $(\ccsstrongbisim)$, the strongest of the three
  relations, holds.

  Consider $\RR = \{(C, \, A\parp B)\}$. The only transitions of $C$ are
  to itself with labels $a$ and $b$: $C \red{a} C$ and $C \red{b} C$.
  Likewise, the only transitions of $A\parp B$ are to itself with
  labels $a$ and $b$: $A\parp B \red{a} A\parp B$ and $A\parp B
  \red{b} A\parp B$.  Therefore $\RR$ is bisimulation.

  
\item $(\ccsstrongbisim)$ does not hold. Take $P = a$. Then the
  second process has the transition $\red{a}$ but the first
  doesn't.
  
  $(\ccsobscong)$ does hold (hence so does $(\ccsweakbisim)$). We
  consider the labelled transitions of each side. We will rely
  once on the rule
  % 
  \begin{gather}
    Q \ccsweakbisim \taup Q
    \label{wktau}
  \end{gather}
  and the fact that $\ccsweakbisim$ is closed by parallel composition.
  
  \begin{itemize}
  \item The only transition of first process
    is $\taup {(P \parp P)} \red{\tau} P \parp P$.  The second process
    can match this transition to the identical target $P\parp\taup P
    \red{\tau} P\parp P$.
    
  \item There are two classes of transitions for the second process.
    \begin{description}
    \item[Case $P \parp \taup P \red{\tau} P \parp P$:]  As seen just
      above the first process can match this transition to the
      identical target.
      
    \item[Case $P \parp \taup P \red{\alpha} P' \parp \taup P$ where $P
      \red{\alpha} P'$:]  The first process can match this
      transition with $\taup {(P \parp P)} \red{\tau}\red{\alpha} P'
      \parp P$. By \eqref{wktau}, $P' \parp \taup P \ccsweakbisim P'
      \parp P$, as desired.
    \end{description}
  \end{itemize}
  
\item None of the relations holds.  Suppose for contradiction that
  $(\ccsweakbisim)$ held.  Take $P = Q = \zinact x$.  The first
  process may undergo two $\tau$ transitions and reach a deadlocked state:
  \begin{gather*}
    \newp a {(\newp b {(\zoutact a \parp \zoutact b \parp \zinp a
        {\zinp b P} \parp \zinp b {\zinp a Q} )})}
    \red{\tau}\red{\tau}
    \newp a {(\newp b {(\zerop \parp \zerop \parp 
        {\zinp b P} \parp {\zinp a Q} )})}
    \ccsstrongbisim
    \zerop
  \end{gather*}
  By hypothesis the second process can match this state with a
  sequence of $0$ or more $\tau$ transitions; only two target states
  are possible:
  \begin{gather*}
    \taup {\zinact x} + \taup {\zinact x}
    \qquad \qquad \zinact x
  \end{gather*}
  but neither is deadlocked since both can do
  $\redstar{\tau} \red{\zinact x}$, a contradiction.
  
  Note: the question should have had the side condition $\{a,b\} \cap
  (\fn P \cup \fn Q) = \emptyset$.  In the absence of this side condition,
  there is a simpler counterexample. Take $P=\zinact a$. Then
  the second process can do $\red{\tau}\red{\zinact a}$ but the first
  process can never have an $\zinact a$ transition.

\item Trick question! None of the relations holds. Take $a=b$. Then
  $\zinp a \zerop$ has an $\zinact a$ transition but the other process
  is weakly bisimilar to $\zerop$.

  Let us assume that the examiner meant to include the side condition
  $a \neq b$. Then we can answer the question as follows...

  The relation $\ccsobscong$ doesn't hold (hence neither does
  $\ccsstrongbisim$).  This is because $\newp b {(A
    \parp B)}$ can do a $\tau$ transition to itself, but $\zinp a
    \zerop$ has no $\tau$ transitions.

    The relation $\ccsweakbisim$ does hold, as illustrated by the red
    dotted lines relating the states of two reduction graphs.  Note
    that we show all the states up to structural equivalence.

    \dotdia{ABgraph}

\item None of the relations holds. Suppose for contradiction that
  $(\ccsweakbisim)$ held.  We have $A \red{\tau} B$. By hypothesis,
  $\zinp a \zerop \ccsweakbisim B$, but this is impossible because
  $\zinp a \zerop$ can have an $a$ transition while $B \ccsweakbisim
  \zerop$, a contradiction.

\end{enumerate}

\section*{Question 2}

They are weakly bisimilar, as illustrated by the red dotted lines
relating the states of two reduction graphs.  Since neither $U$ nor
$U'$ have any initial $\tau$ transitions, $U \ccsobscong U'$, as
desired.

Note that we omit writing the new bindings in all states in the
complex graph in order to save space. Also, we show all the states up to
structural equivalence.

\dotdia{workshop}

\section*{Question 3}
\newcommand{\name}[1]{\mathit{#1}}

We shall use the following name vectors (``left'', ``right'', ``mid'')
throughout:
% 
\begin{align*}
\lvec &= \langle \name{empty}, \name{in}, \name{out}\rangle \\
\rvec &= \langle e, i, o \rangle \\
\mvec &= \langle e', i', o' \rangle
\end{align*}
%
Then the concatenation of cells can be easily written as:
%
\begin{gather*}
 P \pipep Q =
 \pabs {\lvec,\rvec} {\newp \mvec {(
     \pconcr P {\lvec,\mvec}
     \parp
     \pconcr Q {\mvec,\rvec}
     )}}
\end{gather*}

\begin{enumerate}
\item For $C' \pipep C$, we calculate as follows:
  % 
  \begin{mulprf}
    &\pconcr {(C' \pipep C)} {\lvec,\rvec}
    \\
    =&
    \newp \mvec {(
      \pconcr {C'} {\lvec,\mvec}
      \parp
      \pconcr C {\mvec,\rvec}
      )}
    &definition of $\pipep$
    \\
    =&
    \newp \mvec {(
      (
      \zinp {o'} {\pconcr C {\lvec,\mvec}}
      + \zoutp {e'} {\pconcr E {\lvec,\mvec}}
      )
      \parp
      (
      \zoutp {o'} {\pconcr {C'} {\mvec,\rvec}}
      +
      \zinp {i'} {\pconcr {(C \pipep C)} {\mvec,\rvec}}
      )
      )}
    &definition of $C'$ and $C$
    \\
    \red{\tau}&
    \newp \mvec {(
      \pconcr C {\lvec,\mvec}
      \parp
      \pconcr {C'} {\mvec,\rvec}
      )}
    &synchronisation on $o'$
    \\
    =&
    \pconcr {(C \pipep C')} {\lvec,\rvec}
    &definition of $\pipep$
  \end{mulprf}%
  %
  Since the transition shown above is the only one possible (all
  others are prevented by the outermost new binding), we conclude $C'
  \pipep C \ccsweakbisim C \pipep C'$, as desired.

  For $C' \pipep E$, we calculate as follows:
  % 
  \begin{mulprf}
    &\pconcr {(C' \pipep E)} {\lvec,\rvec}
    \\
    =&
    \newp \mvec {(
      \pconcr {C'} {\lvec,\mvec}
      \parp
      \pconcr E {\mvec,\rvec}
      )}
    &definition of $\pipep$
    \\
    =&
    \newp \mvec {(
      (
      \zinp {o'} {\pconcr C {\lvec,\mvec}}
      + \zoutp {e'} {\pconcr E {\lvec,\mvec}}
      )
      \parp
      (
      \zinp {e'} {\pconcr {E} {\mvec,\rvec}}
      +
      \zinp {i'} {\pconcr {(C \pipep E)} {\mvec,\rvec}}
      )
      )}
    &definition of $C'$ and $E$
    \\
    \red{\tau}&
    \newp \mvec {(
      \pconcr E {\lvec,\mvec}
      \parp
      \pconcr E {\mvec,\rvec}
      )}
    &synchronisation on $e'$
    \\
    =&
    \pconcr {(E \pipep E)} {\lvec,\rvec}
    &definition of $\pipep$
  \end{mulprf}%
  Since the transition shown above is the only one possible (all
  others are prevented by the outermost new binding), we conclude $C'
  \pipep E \ccsweakbisim E \pipep E$, as desired.

  For $E \pipep E$, we calculate as follows:
  \begin{mulprf}
    &\pconcr {(E \pipep E)} {\lvec,\rvec}
    \\
    =&
    \newp \mvec {(
      \pconcr E {\lvec,\mvec}
      \parp
      \pconcr E {\mvec,\rvec}
      )}
    &definition of $\pipep$
    \\
    =&
    \newp \mvec {(
      (
      \zinp {\name{empty}} {\pconcr E {\lvec,\mvec}}
      + \zinp {\name{in}} {\pconcr {(C \pipep E)} {\lvec,\mvec}}
      )
      \parp
      \pconcr E {\mvec,\rvec}
%       (
%       \zinp {e'} {\pconcr {E} {\mvec,\rvec}}
%       +
%       \zinp {i'} {\pconcr {(C \pipep E)} {\mvec,\rvec}}
%       )
      )}
    &definition of $C'$
    \\
    \ccsstrongbisim&
      \zinp {\name{empty}}
            { \newp {\mvec} {( \pconcr E {\lvec,\mvec}
                               \parp
                               \pconcr E {\mvec,\rvec}
                             )}}
    + \zinp {\name{in}}
            { \newp {\mvec} {( \pconcr {(C \pipep E)} {\lvec,\mvec}
                               \parp
                               \pconcr E {\mvec,\rvec}
                             )}}
    &expansion
    \\
    \ccsstrongbisim&
      \zinp {\name{empty}}
            { \pconcr {(E \pipep E)} {\lvec,\rvec}}
    + \zinp {\name{in}}
            { \pconcr {(C \pipep ( E \pipep E ))} {\lvec,\rvec}}
    &definition of $\pipep$ and associativity 
  \end{mulprf}%
  Therefore $E$ and $E \pipep E$ satisfy the same guarded recurrences,
  hence $E \ccsstrongbisim E \pipep E$, as desired.


\item We now show that $C' \pipep C^{(k)} \ccsweakbisim C^{(k)}$ for
  $0 \leq k$. We induct on $k$.
  \begin{description}
    \item[Base case:] We calculate:
      % 
      \begin{mulprf}
        & C' \pipep C^{(0)}
        \\
        =& C' \pipep E &definition
        \\
        \ccsweakbisim& E \pipep E &previous exercise
        \\
        \ccsstrongbisim& E &previous exercise
        \\
        =&  C^{(0)}  &definition
      \end{mulprf}%
      Since $(\ccsstrongbisim) \subseteq (\ccsweakbisim)$, we have
      % 
      $C' \pipep C^{(0)} \ccsweakbisim C^{(0)}$ as desired.

    \item[Step case:] We calculate:
      \begin{mulprf}
        & C' \pipep C^{(k+1)}
        \\
        =& C' \pipep (C \pipep C^{(k)})  &definition
        \\
        \ccsstrongbisim& (C' \pipep C) \pipep C^{(k)}  &associativity
        \\
        \ccsweakbisim& (C \pipep C') \pipep C^{(k)}  &previous
        ex; also $\ccsweakbisim$ closed by $\pipep$
        \\
        \ccsweakbisim& C \pipep C^{(k)}  &inductive hypothesis
        \\
        =&  C^{(k+1)}  &definition
      \end{mulprf}%
      Since $(\ccsstrongbisim) \subseteq (\ccsweakbisim)$, we have
      % 
      $C' \pipep C^{(k)} \ccsweakbisim C^{(k)}$ as desired.      

    \end{description}
    
  \item First we consider the base case:
%
    \begin{mulprf}
      & \pconcr {C^{(0)}} {\lvec,\rvec}
      \\
      =& \pconcr E {\lvec,\rvec}
      &definition
      \\
      =& \zinp {\name{empty}} {\pconcr E {\lvec,\rvec}}
      + \zinp {\name{in}} {\pconcr {(C \pipep E)} {\lvec,\rvec}}
      &definition
      \\
      =& \zinp {\name{empty}} {\pconcr { C^{(0)} } {\lvec,\rvec}}
      + \zinp {\name{in}} {\pconcr {C^{(1)}} {\lvec,\rvec}}
      &definition
    \end{mulprf}%
    Then we consider the other case:
    \begin{mulprf}
      & \pconcr {C^{(k+1)}} {\lvec,\rvec}
      \\
      =& \pconcr {(C \pipep C^{(k)})} {\lvec,\rvec} &definition
      \\
      \ccsstrongbisim&
      \zoutp {\name{out}}
             {\pconcr {(C' \pipep C^{(k)})}  {\lvec,\rvec} }
      +\zinp {\name{in}}
             {\pconcr {((C \pipep C) \pipep C^{(k)})} {\lvec,\rvec} }
      &expansion
      \\
      \ccsstrongbisim&
      \zoutp {\name{out}}
             {\pconcr {C^{(k)}}  {\lvec,\rvec} }
      +\zinp {\name{in}}
             {\pconcr {((C \pipep C) \pipep C^{(k)})} {\lvec,\rvec} }
      &previous exercise
      \\
      \ccsstrongbisim&
      \zoutp {\name{out}}
             {\pconcr {C^{(k)}}  {\lvec,\rvec} }
      +\zinp {\name{in}}
             {\pconcr {C^{(k+2)}} {\lvec,\rvec}  }
      &associativity and definition of $C^{(k+2)}$
    \end{mulprf}
    We have show that the families $C^{(k)}$ and $B_k$ satisfy the same
    guarded recurrences, hence $C^{(k)} \ccsweakbisim B_k$ for
    all $0 \leq k$.  
  \end{enumerate}
\end{document}

