\documentclass[11pt]{article}
\usepackage{a4}
\usepackage{amsfonts}

\input{leifer-exam-macros}
\usepackage{geometry}
\geometry{%
  dvips, a4paper,
  left=20mm, right=20mm,
  top=20mm, bottom=20mm, %
}   

\title{\vspace{-.5cm}{\LARGE\bf MPRI 2004/05 -- Cours 2-3 (Concurrency)}}
\author{\LARGE \bf Exam}
\date{\vspace{-.1cm}17 February 2005}

\begin{document}

\maketitle
\thispagestyle{empty}

\begin{center}
{\large\bf Part I - CCS}
\end{center}
\paragraph*{Question 1}

For each of the following pairs of processes, say which is
the strongest relation which relates them, among $\sim$, $\approx$ and
$\cong$. Justify your answer, namely prove that the relation holds
and that no stronger relation holds. Note: In some case, it may be
that none of the relations holds

\begin{enumerate}
\item $\tau.P$ \ and \  $P + \tau.P$  
\item  $P$  \ and \   $P \mid P$ 
\item  $A$ \ and \ $B$, \ where \ $A$ \ and \ $B $ are defined recursively by 
$A = a.A$ \  and \  $B = a.B \,| \,a.B$. 
\item  $ (\nu b) (a.b.c.0 \,|\,d.\bar b.e.0)$ \  and \  $a.c.0 \,|\, d.e.0$ 
\item  $P + Q$ \ and \ $\tau.P + \tau.Q$ 
\item  $(\nu a)(\bar a \, | \,(a.P + a.Q))$ \ and \  $\tau.P + \tau.Q$ 
\end{enumerate}

\paragraph*{Question 2}

We say that $P$ {\it simulates} $Q$, notation $Q\preceq P$, 
if there exists a relation $\cal R$ such that $(Q,P)\in {\cal R}$ 
and for every $(T,U)\in {\cal R}$ we have:
\[T \stackrel{\alpha}{\longrightarrow}T' \;\; \mbox{\it implies} \;\;\exists U' .\,
U \stackrel{\alpha}{\longrightarrow}U' \; \mbox{\it and} \;  (T',U')\in {\cal R}
\]
Say whether it is the case that $P \sim Q$ if 
and only if $P\preceq Q$ and $Q \preceq P$. 
Justify your answer, namely prove the above equivalence 
or find a counterexample


\vspace{1cm}
\begin{center}
{\large\bf Part II - The Pi-calculus}
\end{center}


  \begin{enumerate}

  \item The monadic synchronous \pic{} has the following grammar:
    % 
    \begin{gather*}
      P
      \quad
      ::= 
      \quad \outp x y P
      \synbar \inp x y P 
      \synbar \newp x P  
      \synbar \zerop
      \synbar P \parp P  
      \synbar \bangp P   
    \end{gather*}
    % 
    
  \item The following labelled transition rules give the behavior of
    replication:
    % 
    \begin{gather}
      \infer
      {P \red{\alpha} P'}{\bangp P \red{\alpha} P' \parp \bangp P}%
      \text{if $\bn \alpha \cap \fn P = \emptyset$}
      \quad\eqtag{bang-spawn}
      \\[2ex]
      \infer
      {P \red{\outlab x y } P' \qquad P \red{\inlab x y } P''}%
      {\bangp P \red{\tau} (P' \parp P'') \parp \bangp P}
      \quad\eqtag{bang-comm}
      \\[2ex]
      \infer{P \red{\boutlab x y } P' \qquad P \red{\inlab x y } P''}%
      {\bangp P \red{\tau} \newp y {(P' \parp P'')} \parp \bangp P}%
      \text{if $y \notin \fn P$}
      \quad\eqtag{bang-close}
    \end{gather}
    
  \end{enumerate}
  
 \paragraph*{Question 3}
  
   Define what it means for a relation to be a strong labelled
    bisimulation.
        
%   \item In the monadic \pic{}, prove that replication distributes
%     through parallel composition, \ie %
%     $\bangp (P \parp Q) \strongbisim \bangp P \parp \bangp Q$, by
%     finding a relation containing them and showing that this relation
%     is a strong labelled bisimulation.


\paragraph*{Question 4}
    In the monadic \pic{}, prove that strong labelled bisimilarity
    is preserved by replication, \ie %
    $P \strongbisim Q$ implies $\bangp P \strongbisim \bangp Q$.
    To do this, construct an explicit relation $\RR$ that contains the
    latter pairs (amongst others) and prove that it is a strong
    labelled bisimulation.

    Note: You may use the fact that $\strongbisim$ is preserved by
    parallel composition and by new binding, but if you do, cite the
    these results clearly.

    You may use ``up to'' techniques; if so explain clearly how and
    where you use them.

%   \item (Comment: a good solution will give an explicit definition of
%     the relation; will do the bisimulation proof in both directions;
%     will be careful about side conditions; will quote the bang LTS
%     rules explicitly; and will be explicit about how and where ``up
%     to'' techniques are being used.)
  
%%    A relation $\RR$ is a strong labelled bisimulation iff it is
%%    symmetric and 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$.

%     Let %
%     $\RR = \{ \bangp (P \parp Q) \strongbisim \bangp P \parp \bangp Q
%     \setst \text{$P,Q$ are processes} \}$.

%     \begin{description}
%     \item [$\RR$ is a simulation:] Suppose $\bangp (P \parp Q)
%       \red{\alpha} S$ and $\bn \alpha \cap \fn {\bangp P \parp \bangp
%         Q} = \emptyset$, \ie
%       % 
%       \begin{gather}
%         \bn \alpha \cap (\fn P \cup \fn Q) = \emptyset \label{eq:hyp1}
%       \end{gather}
%       %
%       The possible case are as follows.  The side conditions
%       concerning $\bn \alpha$ in the following analysis are all
%       implied by the hypothesis \eqref{eq:hyp1}, so omitted:

%       \begin{description}
%       \item[\maketag{bang-spawn}:] We have $P \parp Q \red{\alpha}
%         S_0$ for some $S_0$ and $S = S_0 \parp \bangp {(P \parp Q)}$.
%         This could be due to:
%         \begin{description}
%           \item  $P$ acting alone: TODO

%           \item $Q$ acting alone: TODO

%           \item $P$ and $Q$ communicating: TODO
%         \end{description}

%       \item[\maketag{bang-comm}:] TODO

%       \item[\maketag{bang-close}:] TODO

%       \end{description}

%     \item [$\RR^{-1}$ is a simulation:]
%     \end{description}
    

\vspace{1cm}
\begin{center}
{\large\bf Part III - The Asynchronous Pi-calculus}
\end{center}
  \begin{enumerate}
    
  \item The monadic \emph{asynchronous} \pic{} has the following
    grammar:
    % 
    \begin{gather*}
      P
      \quad
      ::= 
      \quad \outact x y
      \synbar \inp x y P 
      \synbar \newp x P  
      \synbar \zerop
      \synbar P \parp P  
      \synbar \bangp P   
    \end{gather*}
    
  \item The set of \emph{evaluation contexts} $\EvalCxt$ is defined
    as
    % 
    \begin{gather*}
      \EvalCxt =
      \{ \newp \zvec {(- \parp T)} \quad\setst\quad \text{$T$ a process} \}
    \end{gather*}
    % 
    where the \emph{binding names} of $D = \newp \zvec {(- \parp T)} \in
    \EvalCxt$ are $\bind D = \{\zvec\}$.
    
  \item \emph{Reduction} and \emph{strong barbs} are both
    characterisable in terms of evaluation contexts and structural
    congruence:
    % 
    \begin{itemize}
    \item $P \red{} P'$ iff there exists $D \in \EvalCxt$, names $x$,
      $v$, and $u$, and a process $P_0$ such that %
      $P \streq D[\outact x v \parp \inp x u {P_0}]$ and %
      $P' \streq D[\sub v u {P_0}]$.
      
    \item $P \barb x$ iff there exists $D \in \EvalCxt$ and names $x$
      and $v$ such that $P \streq D[\outact x v]$ and $x \notin \bind D$.
    \end{itemize}
    
  \item \emph{Weak barbed bisimulation} $\weakbbisim$ is the largest
    relation $\RR$ that is symmetric and for which for all $(P,Q)
    \in \RR$ %
    \begin{itemize}
    \item if $P \red{} P'$, there exists $Q'$
      such that $Q \redstar{} Q'$ and $(P',Q') \in \RR$;
      
    \item if $P \barb x$ then $Q \wbarb x$.
    \end{itemize}
  \end{enumerate}
  
\paragraph*{Question 5}
\begin{enumerate}
\item Define the weak barb relation $Q \wbarb x$ used above in the
    definition of $\weakbbisim$.
    
  \item Show why $\weakbbisim$ is not preserved by parallel
    composition, \ie find $P,Q,R$ such that $P \weakbbisim Q$ but
    not %
    $P \parp R \weakbbisim Q \parp R$.

  \item Prove that $P \red{} P'$ implies $\sub x y P \red{} \sub x y
    {P'}$.

  \item Consider an \emph{equator} process
    %
    \begin{gather*}
      E_{x,y} = %
      \bangp {\inp x u {\outact y u}} %
      \parp \bangp {\inp y u {\outact x u}}
    \end{gather*}
    
  \item Prove that $E_{x,y} \parp D[\outact x v] \red{} E_{x,y} \parp
    D[\outact y v]$ for $x,y \notin \bind D$.

  \item Show that equators can act like substitutions, \ie %
    $\newp y {(E_{x,y} \parp P )} \weakbbisim \sub x y P$.  To do
    this, you need to demonstrate that there exists a weak barbed
    bisimulation containing the pair of processes in question.

  \item Show that in the monadic \emph{synchronous} \pic{}, \ie the
    calculus where output prefixing $\outp w z Q$ is allowed, that
    this is false.  To do this exhibit a concrete $P$ for which the
    barbed behaviour of $\newp y {(E_{x,y} \parp P )}$ differs from
    that of $\sub x y P$.
  \end{enumerate}


\end{document}
