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

@[simp]

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

P | 𝟎 ~ P

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

P | Q ~ Q | P

@[simp]

theorem Cslib.CCS.bisimilarity_nil_par {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {p : Process Name Constant} : (Process.nil.par p) ~[lts] p

𝟎 | P ~ P

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

P | (Q | R) ~ (P | Q) | R

theorem Cslib.CCS.bisimilarity_choice_nil {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {p : Process Name Constant} : (p.choice Process.nil) ~[lts] p

P + 𝟎 ~ P

theorem Cslib.CCS.bisimilarity_choice_idem {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {p : Process Name Constant} : (p.choice p) ~[lts] p

P + P ~ P

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

P + Q ~ Q + P

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

P + (Q + R) ~ (P + Q) + R

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

P Q → μ.P μ.Q

theorem Cslib.CCS.bisimilarity_congr_res {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {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 Cslib.CCS.bisimilarity_congr_choice {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} {p q r : Process Name Constant} : p ~[lts] q → (p.choice r) ~[lts] (q.choice r)

P Q → P + R Q + R

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

P Q → P | R Q | R

theorem Cslib.CCS.bisimilarity_congr {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} (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.