Simulation and bisimulation for the pi-calculus

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.thm]

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

%%
%% Given that the meta-logic of Abella is intuitionistic, the
%% specification of bisimulation here corresponds to open bisimulation.
%%
%% Here we prove here that simulation is preorder and bisimulation is an
%% equivalence relation.

Specification "finite-pic".

% Simulation defined

CoDefine sim : proc -> proc -> prop by
  sim P Q :=
    (forall A P1, {one P A P1} -> exists Q1, {one Q A Q1} /\ sim P1 Q1) /\
    (forall X M, {oneb P (dn X) M} -> exists N, {oneb Q (dn X) N} /\
                                                forall W, sim (M W) (N W)) /\
    (forall X M, {oneb P (up X) M} -> exists N, {oneb Q (up X) N} /\
                                                nabla w, sim (M w) (N w)).

% Simulation is a preorder

Theorem sim_refl : forall P, sim P P.

Theorem sim_trans : forall P Q R, sim P Q -> sim Q R -> sim P R.

% Bisimulation defined

CoDefine bisim : proc -> proc -> prop by
  bisim P Q :=
    (forall A P1, {one P A P1} -> exists Q1, {one Q A Q1} /\ bisim P1 Q1) /\
    (forall X M, {oneb P (dn X) M} -> exists N, {oneb Q (dn X) N} /\
                                                forall W, bisim (M W) (N W)) /\
    (forall X M, {oneb P (up X) M} -> exists N, {oneb Q (up X) N} /\
                                                nabla w, bisim (M w) (N w)) /\
    (forall A Q1, {one Q A Q1} -> exists P1, {one P A P1} /\ bisim Q1 P1) /\
    (forall X N, {oneb Q (dn X) N} -> exists M, {oneb P (dn X) M} /\
                                                forall W, bisim (N W) (M W)) /\
    (forall X N, {oneb Q (up X) N} -> exists M, {oneb P (up X) M} /\
                                                nabla w, bisim (N w) (M w)).

% Bisimulation is an equivalence

Theorem bisim_refl : forall P, bisim P P.

Theorem bisim_sym : forall P Q, bisim P Q -> bisim Q P.

Theorem bisim_trans : forall P Q R, bisim P Q -> bisim Q R -> bisim P R.