\documentclass[11pt]{article}
\newif\ifslidegeometry
\slidegeometryfalse
\newif\ifanswermode
\answermodefalse
%\input{lecture-pre}
\input{common}
\begin{document}
%\huge

\newcommand{\dateoflecture}{16 November 2004}
\setfooters{\dateoflecture}

\begin{center}
  {\bf MPRI Concurrency (course number 2-3) 2004-2005:}\\
  {\bf \pic}
  \\
  {\bf Exercises}
  \\
  \dateoflecture
  \\
  http://pauillac.inria.fr/$\sim$leifer/teaching/mpri-concurrency-2004/ 
  \\
  James J. Leifer 
  \\
  INRIA Rocquencourt
  \\
  James.Leifer@inria.fr
  \\
\end{center}


\begin{enumerate}
\item Consider the term $\bangp {(\inp x w {\outact z w})} \parp
  \outact x x \parp \inp x y {\newp v {\outact y v}}$. You may assume
  that all bound names are distinct from each other and from all free
  names.

  \begin{enumerate}
  \item Show all possible labelled transitions of this process.
  \item Show the derivation trees for these.
  \end{enumerate}


\item Demonstrate the necessity of the side condition $\bn(\alpha)
  \cap \fn(Q) = \emptyset$ in the rule \maketag{lab-par-l}. To do so,
  suppose this side condition were deleted.  Now find a process $P$
  such that $P \red{\tau}\red{\tau}$ and for which after alpha
  converting it to $P'$, it is not the case that $P'
  \red{\tau}\red{\tau}$.

\item The coding I gave in the slides of synchronous \pic{} in terms
  of asynchronous \pic{} is unsatisfactory (despite my claim
  otherwise).  The problem is that the translation uses asynchronous
  \emph{polyadic} \pic{} (\eg $\polyoutact x {y,z}$), not asynchonous
  monadic \pic, which was the original goal.
  
  \begin{enumerate}
  \item Show that the original goal can be achieved by defining a
    translation $\trans{-}$ from synchronous monadic \pic{} directly
    to asynchronous monadic \pic{}.
    
  \item Show the reduction steps of %
    $\trans{\outp x y P \parp \inp x u Q}$.
  \end{enumerate}
  
  \answer{
    \begin{enumerate}
    \item Define $\trans{-}$ as follows:
      % 
      \begin{align*}
        \trans{\outp x y P} %
        &= \newp z {(\outact x z \parp \inp z w {(\outact w y \parp
            \trans{P})})} \qquad \text{for $z,w \notin \fn(P)$}
        \\
        \trans{\inp x u Q} %
        &= \inp x {z'} {\newp {w'} {(\outact {z'} {w'} \parp \inp {w'}
            u {\trans{Q}})}} \qquad \text{for $z',w' \notin \fn(Q)$}
      \end{align*}
    \item Suppose $z,z',w,w'$ are fresh and distinct. We have:
      % 
      \begin{align*}
        & \trans{\outp x y P \parp \inp x u Q} \\
        {}={}& \newp z {(\outact x z \parp \inp z w {(\outact w y \parp
            \trans{P})})} \parp \inp x {z'} {\newp {w'} {(\outact {z'} {w'} \parp \inp {w'} u
            {\trans{Q}})}} \\
        {}\streq{}&
      \end{align*}
    \end{enumerate}
  }
  
\item Consider the definition of strong bisimilarity given in the
  slides:
  % 
  \begin{quote}
    A relation $\RR$ is a strong bisimulation if for all $(P,Q) \in
    \RR$ and $P \red{\alpha} P'$, where $\bn(\alpha) \cap \fn(Q) =
    \emptyset$, there exists $Q'$ such that $Q \red{\alpha} Q'$ and
    $(P',Q') \in \RR$, and symmetrically.
    
    Strong bisimilarity $\strongbisim$ is the largest strong
    bisimulation.
  \end{quote}
  % 
  Let $\strongbisim'$ be exactly the same except we omit the side
  condition $\bn(\alpha) \cap \fn(Q) = \emptyset$.
  
  \begin{enumerate}
  \item Is one included in the other, \ie $(\strongbisim) \subseteq
    (\strongbisim')$ or $(\strongbisim') \subseteq (\strongbisim)$?
    
  \item Are they equal? If not, find a pair of processes $(P,Q)$
    that distinguish the relations, \ie $P \strongbisim Q$ but not $P
    \strongbisim' Q$ or vice versa.
  \end{enumerate}
  
  \answer{
    \begin{enumerate}
    \item The inclusion $(\strongbisim') \subseteq (\strongbisim)$
      holds because $\strongbisim'$ satisfies the condition for
      strong bisimulation. To see why, suppose $P \strongbisim' Q$
      and $P \red{\alpha} P'$ and $\bn(\alpha) \cap \fn(Q) =
      \emptyset$. Then by the definition of $\strongbisim'$ (without
      needing to appeal the side condition at all), there exists $Q'$
      such that $Q \red{\alpha} Q'$ and $P' \strongbisim' Q'$. The
      result then follows by symmetry.
      
    \item Since $(\strongbisim') \subseteq (\strongbisim)$, the only
      way we can show they are not equal is by finding $(P,Q)$ such
      that $P \strongbisim Q$ and $P \not\strongbisim' Q$. Take
      % 
      \begin{align*}
        P &= \newp y {\outact x y} \\
        Q &= P \parp \newp w {\outact w y } 
      \end{align*}
      
    \end{enumerate}
  }
\end{enumerate}
\end{document}
