Bisimilarity-up-to for the synchronous pi-calculus

Reasoning

[View pic_core.thm]

Click on a command or tactic to see a detailed view of its use.

%%%
%%%
%%% For more details, please see the paper:
%%%
%%%   "A lightweight formalization of the meta-theory of
%%%   bisimulation-up-to" by K. Chaudhuri, M. Cimini, and
%%%   D. Miller, 2014

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Processes

Kind name,proc type.

%% action prefixes
Type taup         proc -> proc.
Type inp          name -> (name -> proc) -> proc.
Type oup          name -> name -> proc -> proc.

%% name restriction
Type nu           (name -> proc) -> proc.

%% replication
Type repl         proc -> proc.

%% core process algebra
Type plus, par    proc -> proc -> proc.
Type null         proc.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Labels of the LTS

Kind label type.

Type tau          label.
Type up, dn       name -> name -> label.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% The steps of the LTS

% The steps are defined by a mutually inductive definition of a relation
% one for closed steps and oneb for bound steps, i.e., steps that contain
% a name that is restricted (nu) or bound (inp) in an outer scope.

Define
   one  : proc -> label -> proc -> prop,
   oneb : proc -> (name -> label) -> (name -> proc) -> prop
by
   /* internal steps */
;  one (taup P) tau P

   /* closed output */
;  one (oup X Y P) (up X Y) P

   /* core process algebra */
;  one (plus P Q) L R := one P L R
;  one (plus P Q) L R := one Q L R
;  one (par P Q) L (par R Q) := one P L R
;  one (par P Q) L (par P R) := one Q L R
;  one (repl P) L (par (repl P) R) := one P L R
;  one (nu P) L (nu Q) := nabla x, one (P x) L (Q x)

   /* closed communication */
;  one (par P Q) tau (par PP QQ) :=
      /* case of P getting input */
      (exists X Y R, oneb P (dn X) R /\ one Q (up X Y) QQ /\ PP = R Y)
      /* case of Q getting input */
   \/ (exists X Y R, one P (up X Y) PP /\ oneb Q (dn X) R /\ QQ = R Y)

   /* internal closed communication in a replicated process */
;  one (repl P) tau (par (repl P) (par PP QQ)) :=
      exists X Y R,
         one P (up X Y) PP
      /\ oneb P (dn X) R /\ QQ = R Y

   /* bound communication */
;  one (par P Q) tau (nu y\ par (PP y) (QQ y)) :=
      /* case of P getting input */
      (exists X, oneb P (dn X) PP /\ oneb Q (up X) QQ)
      /* case of Q getting input */
   \/ (exists X, oneb P (up X) PP /\ oneb Q (dn X) QQ)

   /* internal bound communication in a replicated process */
;  one (repl P) tau (par (repl P) (nu y\ par (PP y) (QQ y))) :=
      exists X, oneb P (up X) PP /\ oneb P (dn X) QQ

   /* bound output */
;  oneb (nu P) (up X) R := nabla y, one (P y) (up X y) (R y)

   /* bound input */
;  oneb (inp X P) (dn X) P

   /* core process algebra for bound labels */
;  oneb (plus P Q) L R := oneb P L R
;  oneb (plus P Q) L R := oneb Q L R
;  oneb (par P Q) L (x\ par (R x) Q) := oneb P L R
;  oneb (par P Q) L (x\ par P (R x)) := oneb Q L R
;  oneb (repl P) L (x\ par (repl P) (R x)) := oneb P L R
;  oneb (nu P) L (y\ nu x\ R x y) := nabla x, oneb (P x) L (R x).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Bisimilarity-up-to

CoDefine bisim_up_to : (proc -> proc -> proc -> proc -> prop) ->
                       proc -> proc -> prop by
  bisim_up_to Tech P Q :=
     (forall L P1, one P L P1 ->
        exists Q1, one Q L Q1 /\
          exists P2 Q2, Tech P1 P2 Q1 Q2 /\
            bisim_up_to Tech P2 Q2)
  /\ (forall X P1, oneb P (dn X) P1 ->
        exists Q1, oneb Q (dn X) Q1 /\
          exists P2 Q2, forall N,
            Tech (P1 N) (P2 N) (Q1 N) (Q2 N) /\
            bisim_up_to Tech (P2 N) (Q2 N))
  /\ (forall X P1, oneb P (up X) P1 ->
        exists Q1, oneb Q (up X) Q1 /\
          exists P2 Q2, nabla x,
            Tech (P1 x) (P2 x) (Q1 x) (Q2 x) /\
            bisim_up_to Tech (P2 x) (Q2 x))
  /\ (forall L Q1, one Q L Q1 ->
        exists P1, one P L P1 /\
          exists P2 Q2, Tech P1 P2 Q1 Q2 /\
            bisim_up_to Tech P2 Q2)
  /\ (forall X Q1, oneb Q (dn X) Q1 ->
        exists P1, oneb P (dn X) P1 /\
          exists P2 Q2, forall N,
            Tech (P1 N) (P2 N) (Q1 N) (Q2 N) /\
            bisim_up_to Tech (P2 N) (Q2 N))
  /\ (forall X Q1, oneb Q (up X) Q1 ->
        exists P1, oneb P (up X) P1 /\
          exists P2 Q2, nabla x,
            Tech (P1 x) (P2 x) (Q1 x) (Q2 x) /\
            bisim_up_to Tech (P2 x) (Q2 x)).

Define refl_t : proc -> proc -> proc -> proc -> prop by
  refl_t P P Q Q.

Define is_sound : (proc -> proc -> proc -> proc -> prop) -> prop by
  is_sound Tech :=
    forall P Q, bisim_up_to Tech P Q -> bisim_up_to refl_t P Q.

Theorem bisim_reflexive : forall P, bisim_up_to refl_t P P.

Theorem bisim_eq_1L : forall P1 P2 Q,
  bisim_up_to refl_t P1 Q -> P1 = P2 -> bisim_up_to refl_t P2 Q.
Theorem bisim_eq_1R : forall P1 P2 Q,
  bisim_up_to refl_t P2 Q -> P1 = P2 -> bisim_up_to refl_t P1 Q.
Theorem bisim_eq_2L : forall P Q1 Q2,
  bisim_up_to refl_t P Q1 -> Q1 = Q2 -> bisim_up_to refl_t P Q2.
Theorem bisim_eq_2R : forall P Q1 Q2,
  bisim_up_to refl_t P Q2 -> Q1 = Q2 -> bisim_up_to refl_t P Q1.

Theorem bisim_symmetric : forall P Q,
  bisim_up_to refl_t P Q ->
  bisim_up_to refl_t Q P.

Theorem bisim_transitive : forall P Q R,
  bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R -> bisim_up_to refl_t P R.