Simulation in the finite pi-calculus is a "pre-congruence"

Executable Specification

[View finite-pic.sig] [View finite-pic.mod]
sig finite-pic.

% Three syntactic types are used: name (for names), action (for
% actions), and proc (for processes).  The type o denotes the type of
% propositions.

% The constructors for proc are 'null', 'taup', 'match', 'plus',
% 'par', and 'nu' denote, respectively, the mull process, the tau
% prefix, match prefix, the non-deterministic choice operator, the
% parallel composition, and the restriction operator of the
% pi-calculus. The input and output prefixes are encoded as in and
% out.

kind name, proc   type.

type null         proc.
type taup         proc -> proc.
type plus, par    proc -> proc -> proc.
type match, out   name -> name -> proc -> proc.
type in           name -> (name -> proc) -> proc.
type nu           (name -> proc) -> proc.

kind action       type.
type tau          action.
type up, dn       name -> name -> action.

% One step transition for free transitions
type one          proc ->          action  ->          proc  -> o.
% One step transition for binding transitions
type oneb         proc -> (name -> action) -> (name -> proc) -> o.

module finite-pic.

% Finite pi-calculus specification

% A specification of the late transition system for the pi calculus.
% This specification involves the bang constructor.

% bound input
oneb (in X M) (dn X) M.

% free output
one (out X Y P) (up X Y) P.

% tau
one  (taup P) tau P.

% match prefix
one  (match X X P) A Q :- one  P A Q.
oneb (match X X P) A M :- oneb P A M.

% sum
one  (plus P Q) A R :- one  P A R.
one  (plus P Q) A R :- one  Q A R.
oneb (plus P Q) A M :- oneb P A M.
oneb (plus P Q) A M :- oneb Q A M.

% par
one  (par P Q) A (par P1 Q) :- one P A P1.
one  (par P Q) A (par P Q1) :- one Q A Q1.
oneb (par P Q) A (x\par (M x) Q) :- oneb P A M.
oneb (par P Q) A (x\par P (N x)) :- oneb Q A N.

% restriction
one  (nu x\P x) A (nu x\Q x)      :- pi x\ one  (P x) A (Q x).
oneb (nu x\P x) A (y\ nu x\Q x y) :- pi x\ oneb (P x) A (y\ Q x y).

% open
oneb (nu x\M x) (up X) N :- pi y\ one (M y) (up X y) (N y).

% close
one (par P Q) tau (nu y\ par (M y) (N y)) :- oneb P (dn X) M , oneb Q (up X) N.
one (par P Q) tau (nu y\ par (M y) (N y)) :- oneb P (up X) M , oneb Q (dn X) N.

% comm
one (par P Q) tau (par (M Y) T) :-  oneb P (dn X) M, one Q (up X Y) T.
one (par P Q) tau (par R (M Y)) :-  oneb Q (dn X) M, one P (up X Y) R.

Reasoning

[View finite-pic-cong.thm]

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

%%
%% (a "pre-congruence" is a congruence without the symmetric relation
%%  requirement).
%%
%% It should be straightforward to extend this script to prove that
%%  (open) bisimulation is a congruence.
%%
%% Eventually, the adjective "finite" should be removed by allowing
%%  the bang operator in pi-calculus expressions.

Specification "finite-pic".
Import "finite-pic". [View finite-pic]

Theorem sim_cong_null :
      sim null null.

Theorem sim_cong_taup :
  forall P Q, sim P Q -> sim (taup P) (taup Q).

Theorem sim_cong_plus :
  forall P Q R S, sim P Q -> sim R S -> sim (plus P R) (plus Q S).
intros. unfold. % Case 1: free action case and then two subcases: left and right of plus intros. case H3. case H1. apply H5 to H4. search. case H2. apply H5 to H4. search. % Case 2: bound input action case and then two subcases: left and right of plus intros. case H3. case H1. apply H6 to H4. search. case H2. apply H6 to H4. search. % Case 3: bound output action case and then two subcases: left and right of plus intros. case H3. case H1. apply H7 to H4. search. case H2. apply H7 to H4. search.
Theorem sim_cong_match : forall P Q X Y, sim P Q -> sim (match X Y P) (match X Y Q). Theorem sim_cong_out : forall P Q X Y, sim P Q -> sim (out X Y P) (out X Y Q). Theorem sim_cong_in : forall P Q X, (forall W, sim (P W) (Q W)) -> sim (in X P) (in X Q). % Now define an invariant inductively Define inv : proc -> proc -> prop by inv P Q := sim P Q ; inv (par P1 P2) (par Q1 Q2) := inv P1 Q1 /\ inv P2 Q2 ; inv (nu P) (nu Q) := nabla x, inv (P x) (Q x). % We could inline this since it only appears once. That is, the % simInv predicate is the result of applying the body of `sim' once % to inv. Define simInv : proc -> proc -> prop by simInv P Q := (forall A P1, {one P A P1} -> exists Q1, {one Q A Q1} /\ inv P1 Q1) /\ (forall X M, {oneb P (dn X) M} -> exists N, {oneb Q (dn X) N} /\ forall W, inv (M W) (N W)) /\ (forall X M, {oneb P (up X) M} -> exists N, {oneb Q (up X) N} /\ nabla w, inv (M w) (N w)). % We now show that 'inv' is a post-fixed point of simulation. Theorem inv_simInv : forall P Q, inv P Q -> simInv P Q. % We can now conclude that inv is a simulation. Theorem inv_sim : forall P Q, inv P Q -> sim P Q. % The fact that inv is a post-fixed point is used to prove the final % two theorems regarding the pre-congruence of sim. Theorem sim_cong_par : forall P Q R S, sim P Q -> sim R S -> sim (par P R) (par Q S). Theorem sim_cong_nu : forall P Q, nabla w, sim (P w) (Q w) -> sim (nu P) (nu Q).