\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 novembre 2005}
\author{\vspace*{-1ex}MPRI -- Cours 2-3}

\begin{document}

\maketitle
\thispagestyle{empty}

\subsection*{Question 1 (5 points)}

\question Parmi les relations de bisimulations ($\sim$, $\wbsim$ et $\wcong$),
trouver la relation la plus précise reliant:

\begin{enumerate}
\item $A\,|\,B$ \ et \  $C$, o\`u \ $A \stackrel{\rm def}{=} a.A$, \ 
 $B \stackrel{\rm def}{=} b.B$ \ et \  $C \stackrel{\rm def}{=} a.C  + b.C$. 
\item  $\tau.(P\,|\,P)$  \ et \   $P \mid \tau.P$.
\item  $ (\nu a) (\nu b) (\bar a.0 \,|\,\bar b.0 \,|\,a.b.P \, | \, b.a.Q)$ 
 \  et \  $\tau.P + \tau.Q$. 
\item  $a.0$ \ et \ $(\nu b)( A\,|\,B)$, o\`u \ 
 $A \stackrel{\rm def}{=} b.A + a.0$  \ et  
 $B \stackrel{\rm def}{=} \bar b.B + \tau.0$.
\item  $a.0$ \ et \  $A$,  o\`u \ $A \stackrel{\rm def}{=} \tau.B + a.0$ \ 
 et \ $B \stackrel{\rm def}{=} \tau.B$.
\end{enumerate}

\subsection*{Question 2 (5 points)}
Dans un atelier 
il y a deux ouvriers qui sont sp\'ecialis\'es dans la peinture : 
chaque ouvrier $W$ re\c{o}it un article non peint $u$, 
en employant sa propre brosse, il donne l'article peint $\bar p$, 
et recommence le cycle.

Formellement l'unit\'e de production $U$ peut \^etre d\'ecrite comme \c{a}: 
\begin{center}
$U \stackrel{\rm def}{=} W\,|\, W$ \ o\`u \ $W  \stackrel{\rm def}{=} u.\bar p. W$ 
\end{center}
Un jour, une des brosses se casse, et tout en attendant un neuf, 
les deux ouvriers décident de partager le restant, après avoir établi
quelques règles pour la synchronisation. C'est \`a dir, chacune d'eux signalera 
avec $\bar a$ sa action de ''brosse prise'', et avec $\bar b$ sa action de ''brosse  dégage\'e''. 
La nouvelle unité de production $U'$ alors peut \^etre d\'ecrite comme \c{a}: 
\begin{center}
$U' \stackrel{\rm def}{=} (\nu a)(\nu b)(W'\,|\,B\,|\,W' )$ \ o\`u \ 
$W'  \stackrel{\rm def}{=} u.\bar a.\bar b.\bar p. W'$ \ et \
$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 (10 points)}
See the english version.
\subsection*{Bonus question (2 points)}
See the English version.
\end{document}
