Behavioural theory of CCS

Main results

• CCS.bisimilarity_congr: bisimilarity is a congruence in CCS

Additionally, some standard laws of bisimilarity for CCS, including:

• CCS.bisimilarity_par_nil: P | 𝟎 ~ P.
• CCS.bisimilarity_par_comm: P | Q ~ Q | P
• CCS.bisimilarity_choice_comm: P + Q ~ Q + P

theorem CCS.bisimilarity_par_nil {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} (p : Process Name Constant) : (p.par Process.nil) ~[lts] p

P | 𝟎 ~ P

theorem CCS.bisimilarity_par_comm {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} (p q : Process Name Constant) : (p.par q) ~[lts] (q.par p)

P | Q ~ Q | P

theorem CCS.bisimilarity_choice_comm {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p q : Process Name Constant} : (p.choice q) ~[lts] (q.choice p)

P + Q ~ Q + P

theorem CCS.bisimilarity_congr_pre {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p q : Process Name Constant} {μ : Act Name} : p ~[lts] q → (Process.pre μ p) ~[lts] (Process.pre μ q)

P ~ Q → μ.P ~ μ.Q

theorem CCS.bisimilarity_congr_res {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p q : Process Name Constant} {a : Name} : p ~[lts] q → (Process.res a p) ~[lts] (Process.res a q)

P ~ Q → (ν a) P ~ (ν a) Q

theorem CCS.bisimilarity_congr_choice {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p q r : Process Name Constant} : p ~[lts] q → (p.choice r) ~[lts] (q.choice r)

P ~ Q → P + R ~ Q + R

theorem CCS.bisimilarity_congr_par {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} {p q r : Process Name Constant} : p ~[lts] q → (p.par r) ~[lts] (q.par r)

P ~ Q → P | R ~ Q | R

theorem CCS.bisimilarity_congr {Name : Type u} {Constant : Type v} {defs : Rel Constant (Process Name Constant)} (c : Context Name Constant) (p q : Process Name Constant) (h : p ~[lts] q) : (c.fill p) ~[lts] (c.fill q)

Bisimilarity is a congruence in CCS.