\documentclass{article}
\usepackage{a4,a4wide}
\usepackage{amsfonts}
\usepackage{amssymb}

%%%%%%%%%%%%%%% redef of \link %%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\link}{\triangleright}
%\newcommand{\link}{\vartriangleright}
%\newcommand{\link}{\rightleftharpoons}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{\vspace*{-10ex}
{\LARGE\bf Midterm Exam}}
\date{30 November 2005}
\author{\vspace*{-1ex}MPRI 2005/06 -- Cours 2-3  (Concurrency)}

\begin{document}

\maketitle
\thispagestyle{empty}

\subsection*{Question 1 (5 points)}

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 $A\,|\,B$ \ and \  $C$, where \ $A \stackrel{\rm def}{=} a.A$, \ 
 $B \stackrel{\rm def}{=} b.B$ \ and \  $C \stackrel{\rm def}{=} a.C  + b.C$. 
\item  $\tau.(P\,|\,P)$  \ and \   $P \mid \tau.P$.
\item  $ (\nu a) (\nu b) (\bar a.0 \,|\,\bar b.0 \,|\,a.b.P \, | \, b.a.Q)$ 
 \  and \  $\tau.P + \tau.Q$. 
\item  $a.0$ \ and \ $(\nu b)( A\,|\,B)$, where \ 
 $A \stackrel{\rm def}{=} b.A + a.0$  \ and  
 $B \stackrel{\rm def}{=} \bar b.B + \tau.0$.
\item  $a.0$ \ and \  $A$,  where \ $A \stackrel{\rm def}{=} \tau.B + a.0$ \ 
 and \ $B \stackrel{\rm def}{=} \tau.B$.
\end{enumerate}

\subsection*{Question 2 (5 points)}
In a ceramic workshop there are two workers that are specialized 
in painting: 
each worker $W$  receives an unpainted item $u$, paints it using its own 
brush, gives back the painted item $\bar p$, and starts the cycle again. 
Formally the production unit $U$ can be described as follows: 
\begin{center}
$U \stackrel{\rm def}{=} W\,|\, W$ \ where \ $W  \stackrel{\rm def}{=} u.\bar p. W$ 
\end{center}
One day, one of the brushes breaks, and while waiting for a new one, the two workers 
decide to share the remaining one, after establishing some simple synchronization rules. 
More precisely, each of them will signal with $\bar a$ his ``take brush'' action, 
and with $\bar b$ his ``release brush'' action. 
The new production unit $U'$ can then be described as follows: 
\begin{center}
$U' \stackrel{\rm def}{=} (\nu a)(\nu b)(W'\,|\,B\,|\,W' )$ \ where \ 
$W'  \stackrel{\rm def}{=} u.\bar a.\bar b.\bar p. W'$ \ and \
 $B \stackrel{\rm def}{=} a.b.B$
\end{center}
The question is: is the new production unit $U'$ observation 
congruent to the old one $U$? Prove or disprove the statement.


\subsection*{Question 3}
Consider the following specification of an unbounded buffer $B_k({\it empty},{\it in},{\it out})$ in CCS, where $k$ represents 
the number of elements that are in the buffer at the moment, and 
${\it empty}$, ${\it in}$, $\overline{\it out}$ represent the possible actions of the buffer:
\begin{itemize}
\item ${\it empty}$: signal that the buffer is empty. Possible only for $B_0$ 
\item ${\it in}$: insert  an element
\item $\overline{\it out}$: output an element. Possible only for $B_k$ with $k>0$. 
\end{itemize}
For simplicity, we abstract from 
the value of the elements. Furthermore, we omit the parameters when they are clear from context, i.e. 
we write $B_k$ instead of $B_k({\it empty},{\it in},{\it out})$.
$$
\begin{array}{lcl}
B_0 &\stackrel{\rm def}{=}& {\it empty}.B_0 + {\it in}.B_1 \\
B_{k+1} &\stackrel{\rm def}{=}& \overline{\it out}.B_{k} + {\it in}.B_{k+2}
\end{array}
$$

We want to implement the buffer using a concatenation of cells, where each cell 
$C({\it empty},{\it in},{\it out},{\it e},{\it i},{\it o})$ will 
contain just one element. A special process $E({\it empty},{\it in},{\it out},{\it e},{\it i},{\it o})$ 
will represent the empty buffer. 
These processes are specified as follows (again, we omit the parameters for simplicity):
$$ 
\begin{array}{lcl}
 E &\stackrel{\rm def}{=}& {\it empty}.E + {\it in}.(C \link E) \\
 C &\stackrel{\rm def}{=}& \overline{\it out}.C' + {\it in}.(C\link C) \\
 C' &\stackrel{\rm def}{=}& {\it o}.C + \overline{\it e}.E
\end{array}
$$
where $C \link E$ is defined by
$$C \link E \stackrel{\rm def}{=} 
(\nu e')(\nu i')(\nu o') (C({\it empty},{\it in},{\it out},e',i',o') \,|\, E(e',i',o',e,i,o))$$
and analogously for $C \link C$, $C \link C'$, etc.

It is known that $\link$ is associative modulo $\sim$. Namely, 
$(P \link Q) \link R \sim P \link (Q \link R)$. Hence in the following we can omit the parentheses and write
$P \link Q \link R$.

\begin{description}
\item[Question 3.1 (3 points)]
Prove that $C' \link C \approx C \link C'$, \ \ \ $C' \link E \approx E \link E$, \ \ \ and  
$E \link E \sim E$. 

Note: You can use the fact that if $P$ has only one transition of the form $P\stackrel{\tau}{\longrightarrow}Q$, 
then $P\approx Q$. 

\item[Question 3.2 (2 points)]
Define $C^{(k)}$ (for $k\geq 0$) as follows:
$$C^{(k)}\stackrel{\rm def}{=}C\link C\link  \ldots \link C \link E   \;\;\;\mbox{(with $C$ repeated $k$ times)}$$
Using the relations  in previous question, prove that for any $k\geq 0$, $C'\link C^{(k)} \approx  C^{(k)}$. 

Note: You can use the fact that $\approx$ is preserved by $\link$, 
i.e. $P \approx Q $ implies $P \link R \approx Q \link R$.

\item[Question 3.3 (5 points)]
Using the result established in previous question, prove that for every $k\geq 0$,  $C^{(k)}\approx B_k$. 

Note: You can use the expansion theorem and the unique fixed-point theorem for weak bisimulation. 
The expansion theorem (in its most general form) says that for any process process $P$ we have
$
P \sim \sum_{P\stackrel{\alpha}{\longrightarrow}P'}\alpha.P'
$.
The unique fixed-point theorem for weak bisimulation says the following: Consider two 
(possibly infinite) families of processes $\vec{P} = P_1, P_2, \ldots$, $\vec{Q} = Q_1, Q_2, \ldots$, 
and a family of contexts $\vec{C}[\;] = C_1[\;], C_2[\;], \ldots$. Assume that each ``hole'' 
in the contexts is strongly guarded (i.e. in the scope of a non-$\tau$ prefix). We have that, if  
$\vec{P}$ and $\vec{Q}$ satisfy $\vec{P}\approx\vec{C}[\vec{P}]$ and $\vec{Q}\approx\vec{C}[\vec{Q}]$, 
then $\vec{P}\approx\vec{Q}$.

\end{description}

\subsection*{Bonus question (2 points)}
A professor announces in class: 
\begin{quote}
{\it Next week there will be a surprise test.}
\end{quote}
The students reply: 
\begin{quote}
{\it Impossible. You cannot give us a surprise test. In fact, you cannot give it on Friday, 
because it is the last day of the week, and we would know by the end of 
Thursday that it is going to be on Friday, 
so it would not be a surprise. Analogously you cannot give it on Thursday, because we know it cannot be on 
Friday, and so by the end of Wednesday we would know that it would be on Thursday, etc.}
\end{quote}
The professor remains silent. 
The students think that they have won the argument and they are happy imagining 
of all the fun things they can do next week instead of preparing for the test. 
Then, the following week, on Wednesday, the professor gives the test, and takes everybody by surprise. 

How would you explain the above apparent paradox? 

\end{document}
