Results on CCS

Executable Specification

[View ccs.sig] [View ccs.mod]
sig ccs.

kind    proc, act      type.

type    a, tau         act .
type    bar            act -> act .

type    null           proc.
type    out            act -> proc -> proc.
type    plus, par      proc -> proc -> proc.
type    mu             (proc -> proc) -> proc.

type    comp           act -> act -> o.
type    step           proc -> act -> proc -> o.

module ccs.

comp A (bar A).
comp (bar A) A.

step (out A P) A P.
step (plus P Q) A P1 :- step P A P1.
step (plus P Q) A Q1 :- step Q A Q1.
step (par P Q) A (par P1 Q) :- step P A P1.
step (par P Q) A (par P Q1) :- step Q A Q1.
step (mu P) A Q :- step (P (mu P)) A Q.
step (par P Q) tau (par P1 Q1) :- comp A B, step P A P1, step Q A Q1.

Reasoning

[View ccs.thm]

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

%%
%% Many of these are taken from Alwen Tiu's PhD thesis

Specification "ccs".

Theorem mu_id_step_absurd : forall A Q,
  {step (mu x\ x) A Q} -> false.

CoDefine sim : proc -> proc -> prop by
  sim P Q :=
    forall A P1, {step P A P1} -> exists Q1, {step Q A Q1} /\ sim P1 Q1.

Theorem sim_mu_par_ext : forall Q Q1,
  {step Q a (par Q Q1)} -> sim (mu x\ out a x) Q.

Theorem sim_mu_par :
  sim (mu x\ out a x) (mu x\ par (out a x) (out a x)).

Theorem sim_refl : forall P,
  sim P P.

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

CoDefine bisim : proc -> proc -> prop by
  bisim P Q :=
    (forall A P1, {step P A P1} -> exists Q1, {step Q A Q1} /\ bisim P1 Q1) /\
    (forall A Q1, {step Q A Q1} -> exists P1, {step P A P1} /\ bisim P1 Q1).

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.