\documentclass[11pt]{article}
\newif\ifslidegeometry
\slidegeometrytrue

\input{lecture-pre}
\input{common}

\begin{document}
\input{common-post}

\input{lecture-post}
\newcommand{\dateoflecture}{2 December 2004}
\setfooters{\dateoflecture}

\begin{slide}

  \vspring
  \vspring

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

  \vspring
  \vspring
\end{slide}

\begin{slide}
  \slidehead{Today's plan}

  \vspring

  \begin{itemize}
  \item exercises from last week
    
    \vspring
    
  \item strong bisimulation ``up to''
    
    \vspring

  \item strong bisimilarity is not a congruence

    \vspring
    
  \item full strong bisimilarity
    
    \vspring
    
  \item the design of operational equivalences

    \vspring

  \item strong barbed bisimulation
  
    \vspring
    
  \item comparison between strong bisimilarity and strong barbed bisimilarity
  \end{itemize}

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Strong bisimulation up to $\streq$ and $\strongbisim$}

  \vspring

  Suppose 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 {\streq}\RR{\streq}$, and
  symmetrically.
%
  \vspring
%
   \begin{gather*}
     \begin{mygraph}
      !s{2}{1}
       [] ([] {P}="0" [r]       [r] {P'}="1" )
      [d] ([] {} [r]            [r] {\cdot}="7" )
      [d] ([] {} [r]            [r] {\cdot}="8" )
      [d] ([] {Q}="4" [r]       [r] {Q'}="5" )
      % 
      "0" (:@[|1.159pt]"1" ^{\alpha} , :@[|1.159pt]@{-}"4"_{\RR})
      "1" (:@[|1.159pt]@{--}"7" ^{\streq})
      "7" (:@[|1.159pt]@{--}"8" ^{\RR})
      "8" (:@[|1.159pt]@{--}"5" ^{\streq})
      "4" (:@[|1.159pt]@{-->}"5" ^{\alpha})        
     \end{mygraph}
     % 
     \qquad     \qquad
     % 
     \begin{mygraph}
      !s{2}{1}
       [] ([] {P}="0" [r]       [r] {P'}="1" )
      [d] ([] {} [r]            [r] {\cdot}="7" )
      [d] ([] {} [r]            [r] {\cdot}="8" )
      [d] ([] {Q}="4" [r]       [r] {Q'}="5" )
      % 
      "0" (:@[|1.159pt]"1" ^{\alpha} , :@[|1.159pt]@{-}"4"_{\RR})
      "1" (:@[|1.159pt]@{--}"7" ^{\strongbisim})
      "7" (:@[|1.159pt]@{--}"8" ^{\RR})
      "8" (:@[|1.159pt]@{--}"5" ^{\strongbisim})
      "4" (:@[|1.159pt]@{-->}"5" ^{\alpha})        
     \end{mygraph}
  \end{gather*}

  \vspring

  Then ${\streq}\RR{\streq}$ is a strong bisimulation.  Likewise for
  $\strongbisim$ in place of $\streq$.  Is $\RR$ also a strong bisimulation?
  % Answer: no, take RR = {(x-|0,0), (0|0)}

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Evaluation contexts}




  \vspring{}
  Let $\EvalCxt$ be the set of \myemph{evaluation contexts}; these are
  generated by the grammar:

  \vspring

  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      D \in \EvalCxt ::= {}
      & -  & \\
      & D \parp P & \\
      & P \parp D  & \\
      & \newp x D 
    \end{tabular}
  \end{center}

  \vspring

  What isn't an evaluation context?
  % Answer: prefixing and replication

  \vspring

\end{slide}


\begin{slide}
  \slidehead{Strong bisimulation up to contexts}  
  \vspring

  Suppose for all $(P,Q) \in \RR$ and $P \red{\alpha} P'$, where
  $\bn \alpha \cap \fn Q = \emptyset$, there exists
  $D \in \EvalCxt$, $P''$, and $Q''$ such that $P' = D[P'']$ and $Q
  \red{\alpha} D[Q'']$ and $(P'',Q'') \in \RR$, and
  symmetrically.

  \vspring

  \begin{gather*}
    \begin{mygraph}
      !s{2.5}{1.8}
      [] ([] {P}="0" [r]       [r] {P'=D[P'']}="1"  [rr] {P''}="7" )
      [d] ([] {Q}="4" [r]       [r] {D[Q'']}="5"   [rr] {Q''}="8" )
      % 
      "0" (:@[|1.159pt]"1" ^{\alpha} , :@[|1.159pt]@{-}"4"_{\RR})
      "7" (:@[|1.159pt]@{--}"8" ^{\RR})
      "4" (:@[|1.159pt]@{-->}"5" ^{\alpha})        
    \end{mygraph}
  \end{gather*}
  
  \vspring


  Then
  $
    \{ (D[P],D[Q]) \setst (P,Q) \in \RR, D \in \EvalCxt \}
  $
  is a strong bisimulation.

  % I ``proved'' this in class by defining RR' to be the above
  % relation and showing the case that D=-|S.  Should
  % think carefully though about the proof methodology though. Are we
  % inducting on D? Hmm...

  \vspring

  Example: $\bangp {\bangp P} \strongbisim \bangp P$.
  
  % This example requires the ``join'' of the two up to techniques.
  % Should explain that.
  \vspring

\end{slide}

\begin{slide}

  \slidehead{Easier reduction rules for replication}

  \vspring

  To prove this example, we use easier reduction rules for replication:
  \vspring

  \begin{gather*}
    \infer
    {P \red{\alpha} P'}{\bangp P \red{\alpha} P' \parp \bangp P}%
    \text{if $\bn \alpha \cap \fn P = \emptyset$}
    \quad\maketag{lab-bang-simple}
    \\[0 pt plus 1fill]
    \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\maketag{lab-bang-comm}
    \\[0 pt plus 1fill]
    \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\maketag{lab-bang-close}
  \end{gather*}
  
  \vspring
  % FIXME: Maybe should have given these from the beginning?
\end{slide}

\begin{slide}
  \slidehead{Congruence?}

  \vspring

  A relation $\RR$ is a \myemph{congruence} if for all $(P,Q) \in \RR$
  and all contexts $C$, we have $(C[P],C[Q]) \in \RR$.
  
  \vspring

  Theorem: Strong bisimilarity, $\strongbisim$, is a congruence with
  respect to all non input-prefixing contexts, \ie $P \strongbisim Q$
  implies $C[P] \strongbisim C[Q]$ where
  % 
    \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      C ::= {}
      & -  & \\
      & C \parp S & \\
      & S \parp C  & \\
      & \newp x C & \\
      & \bangp C & \\
      & \outp x y C 
    \end{tabular}
  \end{center}

  \vspring

  But is it a congruence?
  
  \vspring
  
\end{slide}

\begin{slide}
  \slidehead{Congruences and substitution preservation}
  
  \vspring

  A relation $\RR$ is \myemph{preserved by substitution} if for all
  $(P,Q) \in \RR$ and any substitution $\sigma$, we have %
  $(\sigma P, \sigma Q) \in \RR$.
    
  \vspring

  Claim: If $\RR$ is a strong bisimulation and a congruence then it is
  preserved by substitution.

  \vspring

  To see why, consider the input-prefixing context $C = \inp z y {-}
  \parp \outact z x$.  Suppose $(P,Q) \in \RR$.  Since $\RR$ is a
  congruence, %
  $(C[P],C[Q]) \in \RR$.

  \vspring

  Since $C[P] \red{\tau} \sub x y P$ and $\RR$
  is a bisimulation, $C[Q]$ must be able to match this $\tau$
  transition with the only one it is capable of, namely %
  $C[Q] \red{\tau} \sub x y Q$, and $(\sub x y P, \sub x y Q) \in
  \RR$, as desired.

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Strong bisimilarity is not a congruence}

  \vspring

  By the contrapositive, if $\strongbisim$ is not preserved by 
  substitution, then it is not a congruence.


  \vspring

  \begin{itemize}
  \item Counter example with sum: $\zoutact x \parp \zinact y %
    \strongbisim  %
    \zoutp x {\zinact y} + \zinp y {\zoutact x}$

  \vspring

  \item Counter example with sum: %
    $\newp w {(\zoutp x {\zoutact w} %
      \parp \zinp y {\zinp w {\zoutact a}})} %
    \strongbisim %
    \zoutp x {\zinp y  {\taup {\zoutact a}}} %
    + \zinp y  {\zoutp x {\taup {\zoutact a}}}$ %

    \vspring
    
  \item Counter example without sum:

    \begin{center}
      \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
        & \bangp {(\newp w {(\zoutp x {\zoutact w} %
            \parp \zinp y {\zinp w {\zoutact a}})})} \\
        {} \strongbisim {} &
        \bangp {(\zoutp x {\zinp y  {\taup {\zoutact a}}} %
          + \zinp y  {\zoutp x {\taup {\zoutact a}}})} %
        & by the previous exercise and \eqref{repcong}
        \\
        {} \strongbisim {} &
        \bangp {(\zoutp x {\zinp y  {\taup {\zoutact a}}})} %
        \parp \bangp {(\zinp y  {\zoutp x {\taup {\zoutact a}}})} %
        & by \eqref{sumrep}
      \end{tabular}
    \end{center}
    % 
    where we know that $\strongbisim$ is a congruence with respect to
    replication
    % 
    \begin{gather}
      P \strongbisim Q \mathrel{\text{implies}} \bangp P \strongbisim \bangp Q \label{repcong}
    \end{gather}
    and that replication ``distributes'' through sum:
    \begin{gather}
      \bangp {(\outp x u P + \inp y v Q)} %
      \strongbisim %
      \bangp {\outp x u P} \parp \bangp {\inp y v Q}
      \label{sumrep}
    \end{gather}
  \end{itemize}
  
  \vspring

\end{slide}

\begin{slide}
  \slidehead{Strong bisimilarity and full strong bisimilarity}

  \vspring

  As we've just seen, $\strongbisim$ isn't a congruence with respect
  to input prefixing.

  \vspring

  Definition (full strong bisimilarity): The relation
  $\fullstrongbisim$ is defined as follows.  For all $P$ and $Q$, we
  have that $P \fullstrongbisim Q$ iff for all substitutions $\sigma$,
  $\sigma P \strongbisim \sigma Q$.

  \vspring

  Theorem: $\fullstrongbisim$ is a congruence.

  \vspring

  Proof sketch: The most interesting case is that of input prefixing.
  Suppose $P \fullstrongbisim Q$. We want to show that $\inp x y P
  \fullstrongbisim \inp x y Q$, \ie for all $\sigma$ we have $\sigma
  (\inp x y P) \strongbisim \sigma (\inp x y Q)$.  Assuming $y$ is
  fresh, we can push the substitution in: %
  $\inp {(\sigma x)} y {(\sigma P)} \strongbisim \inp {(\sigma x)} y
  {(\sigma Q)}$. The LHS's only labelled transition $\inp {(\sigma x)}
  y {(\sigma P)} \red{\inlab {(\sigma x)} z} \sub z y {\sigma P}$ is
  matched by a similar one on the RHS to %
  $ \sub z y {\sigma Q}$.  Finally, the hypothesis %
  $P \fullstrongbisim Q$ implies %
  $\sub z y {\sigma P} \strongbisim \sub z y {\sigma Q}$, as desired.

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Operational equivalences and process calculi: from
    automata to compositional languages}

  \vspring

  \sizes

  \begin{description}

  \item 1956: E. F. Moore. ``Gedanken-experiments on sequential
    machines''.

    ``finite automata from the experimental point of view'' --- trace
    refinement and trace equivalence of automata

  \vspring

  \item 1980: R. Milner. \emph{A Calculus of Communicating Systems}.

    a compositional syntax, namely CCS; operational equivalences based
    on bisimulation; congruence results for compositional reasoning.

  \vspring

  \item 1981: D. Park. ``Concurrency and automata on infinite sequences''.

    bisimulation: an operational equivalence that is sensitive to
    nondeterminism.

    \vspring
  

  \item 1989: R. Milner, J. Parrow, and D. Walker. ``A calculus of
    mobile processes, parts I and II''.

    \pic{} without structural congruence or reductions

  \end{description}
  
    \vspring
  
\end{slide}
\begin{slide}

  \slidehead{Operational equivalences and process calculi: from
    labelled transitions to reductions}

 \vspring

 \sizes

  \begin{description}

  \item 1990: G. Berry and G. Boudol. ``The chemical abstract
    machine''

    structural congruence and reduction rules

    \vspring


  \item 1990: R. Milner. ``Functions as processes''.

    (written while visiting INRIA Sophia) structural congruence
    and reduction rules to \pic


    \vspring

  \item 1992: R. Milner and D. Sangiorgi. ``Barbed bisimulation''.

    equivalence based on reduction and observations of ``barbs'', not
    labelled transitions.

    \vspring\vspring
    
  \item \emph{... followed by a wealth of new reduction-based process calculi, \eg}

    \vspring\vspring

  \item 1998: L. Cardelli and A. D. Gordon. ``Mobile ambients''.
    % 
    \begin{gather*}
      n [ \mathsf{in}\, m. P \parp Q] \parp m[R] \red{} m[n[P\parp Q]
      \parp R] \\
      ...
    \end{gather*}

  \item 2003: M. Merro and F. Zappa Nardelli. ``Bisimulation proof
    methods for Mobile Ambients''.

    first LTS for ambients that recovers barbed bisimilarity


  \end{description}

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Operational equivalences based on reduction}

  \vspring

  \begin{itemize}
  \item For all $(P,Q) \in \RR$ and $P \red{} P'$, there exists $Q'$
    such that $Q \red{} Q'$ and $(P',Q') \in \RR$, and vice versa.

    \vspring

    Problem: this definition equates %
    $\outact x y$ and $\zerop$.

    \vspring    \vspring
   
  \item For all $(P,Q) \in \RR$ and $P \red{} P'$, there exists $Q'$
    such that $Q \red{} Q'$ and $(P',Q') \in \RR$, and vice versa;
    moreover, for all $x$, we have $P \barb x$ iff $Q \barb x$.

    \vspring

    We say that $P$ has a \myemph{strong barb} $x$, written $P \barb
    x$ iff there exists $P_0$, $P_1$, and $\yvec$ such that %
    $P \streq \newp {\yvec} {(\outp x u {P_0} \parp P_1)}$ and $x \not\in \yvec$.

    \vspring

    \myemph{Strong barbed barbed bisimilarity} is the largest such $\RR$ and
    is written $\strongbbisim$.

    \vspring

    Problem: $\strongbbisim$ equates %
    $\outact x y$ and $\outact x z$, thus it is not a congruence since
    it distinguishes between $C[\outact x y]$ and  $C[\outact x z]$
    where $C = - \parp \inp x u {\outact u w}$.

  \vspring    \vspring

  \item Strong barbed congruence $\strongbcong$ is the context closure
    of $\strongbbisim$, \ie $P \strongbcong Q$ iff for all contexts
    $C$ we have $C[P] \strongbbisim C[Q]$
  \end{itemize}

  \vspring

\end{slide}

\begin{slide}

\slidehead{Barbs can be simple!}

  \vspring

  Why no input barbs? How do we check that a process $P$ is capable of
  inputting on $x$, \ie that there exists $P_0$, $P_1$, and $\yvec$
  such that %
  $P \streq \newp {\yvec} {(\inp x u {P_0} \parp P_1)}$ and $x \not\in \yvec$?

  Easy! Just use the context $- \parp \outp x v {\outact k w}$ for $k$
  fresh and check for a barb on $k$.

  \vspring

  Are a variety of output barbs even necessary? No. All we need is
  just one (or sometimes two) distinguished observables.  Let us add a
  new construct $\beep$:
  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      P ::= {} &... \\
      & \beep  & \\
    \end{tabular}
  \end{center}
  We can observe that a process beeps, written $P \barb \beep$,
  if there exists $D \in \EvalCxt$, an evaluation context, such that
  $P \streq D[\beep]$.




%   \begin{quote}
%     \tcR{An equivalence should distinguish between two processes if
%       and only if a context of the language can distinguish between
%       them.}
%   \end{quote}
  
%   \vspring

%   What does it mean for a context to distinguish between two
%   processes?

%   \vspring

%   \vspring

%   Now we can say that for two beep-free processes $P$ and $Q$, the
%   context $C$ distinguishes between them iff $C[P] \barb \beep$ but
%   not $C[Q] \barb \beep$, or vice versa.

  Then $P$ has an output barb $x$, \ie $P \barb x$, iff $C[P]
  {\red{}}{\barb \beep}$ where %
    $C = - \parp \inp x u {\beep} $.

\vspring

\end{slide}

\begin{slide}
  \slidehead{Advantages and disadvantages of barbed congruence}

  \vspring

  Advantages: even for complex process calculi, it's easy to work with
  barbs: they're just ``beeps'' or ``print statements''.  Compare this
  to the difficulty of modifying the \pic's labelled transitions to
  cope with polyadic communication, code mobility, etc.

  \vspring

  Disadvantages: the quantification over all contexts is heavy.

  \vspring

\end{slide}

\slidehead{Exercises for next lecture}

\vspring
  
\begin{enumerate}
\item You might have noticed that the ``up to'' technique we used in
  the proof of %
  $\bangp {\bangp P} \strongbisim \bangp P$ %
  was different from those justified by the theorems.  In particular,
  we combined ``up to contexts'' and ``up to structural congruence''
  without justification.  The goal of this exercise is to show some
  general criteria for composing ``up to'' techniques.

   \vspring

  Let us say that a relation $\RR$ \myemph{strongly progresses} to a
  relation $\TT$, written $\RR \strongprog \TT$, 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 \TT$, and symmetrically.
  % 
   \begin{gather*}
     \begin{mygraph}
      !s{1.7}{1.7}
       [] ([] {P}="0" [r]       [r] {P'}="1" )
      [d] ([] {Q}="4" [r]       [r] {Q'}="5" )
      % 
      "0" (:@[|1.159pt]"1" ^{\alpha} , :@[|1.159pt]@{-}"4"_{\RR})
      "1" (:@[|1.159pt]@{--}"5" ^{\TT})
      "4" (:@[|1.159pt]@{-->}"5" ^{\alpha})        
     \end{mygraph}
   \end{gather*}
   
   Next, say that a function $\FF$ on relations \myemph{is strongly safe} if %
   $\RR \subseteq \TT$ and $\RR \strongprog \TT$ %
   implies $\FF(\RR) \subseteq \FF(\TT)$ and $\FF(\RR) \strongprog \FF(\TT)$.

   \vspring

   \newpage

   \begin{enumerate}
   \item Prove that if %
     $\RR \subseteq \RR' \strongprog \TT' \subseteq \TT$ then %
     $\RR \strongprog \TT$.

     \vspring

   \item Consider two families of relations $\{\RR_i \setst i \in I\}$
     and $\{\TT_j \setst j \in J\}$.  Suppose that for all $i \in I$
     there exists $j \in J$ such that $\RR_i \strongprog \TT_j$. Prove
     that $\bigcup_{i\in I} \RR_i \strongprog \bigcup_{j\in J} \TT_j$.

     \vspring

   \item \myemph{Principle of ``up to''}: Prove that if $\FF$ is
     strongly safe and %
     $\RR \strongprog \FF(\RR)$ then $\RR$ and $\FF(\RR)$ are included
     in $\strongbisim$.

     Hint: Let $\RR_i = \RR$ and $\RR_{i+1} = \RR_i \cup \FF(\RR_i)$.
     Let $\RR_{*} = \bigcup_{i \in \mathbb{N}} \RR_i$.  Show that
     $\RR_{*}$ is a bisimulation.

     \vspring

   \item \myemph{Example: structural congruence}: Let %
     $\FF_{\streq}(\RR) = {\streq}{\RR}{\streq}$.  Show that
     $\FF_{\streq}$ is strongly safe.

     \vspring

   \item \myemph{Example: Evaluation contexts}: Let %
     $\FF_{\EvalCxt}(\RR) = \{(D[P],D[Q]) \setst (P,Q) \in \RR \text{\ and\ } %
     D \in \EvalCxt\}.$ Show that $\FF_{\EvalCxt}$ is strongly safe.

     \vspring

   \item \myemph{Composition}: Suppose that $\FF$ and $\FF'$ are
     strongly safe. Show that their composition, $\FF \circ \FF'$ is
     too, where $(\FF \circ \FF')(\RR) = \FF(\FF'(\RR))$.

     \vspring

   \item \myemph{The initial motivation for all this work(!)}: Deduce
     that $\FF_{\streq} \circ \FF_{\EvalCxt}$ is strongly safe and
     give the inferred ``up to'' principle explicitly.
   \end{enumerate}

   \vspring

  \newpage
  
\item Prove $\bangp P \parp \bangp P \strongbisim \bangp P$ using the
  easier derivation rules for replication and the ``up to''
  techniques. (I gave this exercise last week, but now you have all
  the necessary knowledge to do it.)

\item When arguing that bisimilarity isn't preserved by substitution,
  we relied on the following result: $ \bangp {(\outp x u P + \inp y v
    Q)} %
  \strongbisim %
  \bangp {\outp x u P} \parp \bangp {\inp y v Q} $.  Prove it using
  ``up to'' techniques.

  \end{enumerate}

% \begin{slide}
%   \slidehead{A family portrait (strong)}

%   \vspring

%   \begin{tabular}{|l|l|}
%     \hline
%     strong bisimilarity ($\strongbisim$): largest s.t.\\
%     $\begin{mygraph}
%       !s{1.8}{1.8}
%       [] ([] {P}="0" [r]       [r] {P'}="1"  )
%       [d] ([] {Q}="4" [r]       [r] {Q'}="5"  )
%       % 
%       "0" (:@[|1.159pt]"1" ^{\alpha} , :@[|1.159pt]@{-}"4"_{\strongbisim})
%       "1" (:@[|1.159pt]@{--}"5" ^{\strongbisim})
%       "4" (:@[|1.159pt]@{-->}"5" ^{\alpha})        
%     \end{mygraph}$ &
%     strong barbed equivalence ($\strongbequiv$) \\

%   \end{tabular}

%   \vspring

% \end{slide}

\end{document}

%% Local IspellDict: british

%% Local Variables:
%% time-stamp-line-limit: 100
%% time-stamp-format: "%04Y/%02m/%02d %02H:%02M:%02S %u"
%% time-stamp-time-zone: "GMT"
%% End:
