Behavioural theory of CCS

Main results

• CCS.bisimilarityCongruence: 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} : lts.HomBisimilarity (p.par Process.nil) 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} : lts.HomBisimilarity (p.par q) (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} : lts.HomBisimilarity (Process.nil.par p) 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} : lts.HomBisimilarity (p.par (q.par r)) ((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} : lts.HomBisimilarity (p.choice Process.nil) 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} : lts.HomBisimilarity (p.choice p) 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} : lts.HomBisimilarity (p.choice q) (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} : lts.HomBisimilarity (p.choice (q.choice r)) ((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} : lts.HomBisimilarity p q → lts.HomBisimilarity (Process.pre μ p) (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} : lts.HomBisimilarity p q → lts.HomBisimilarity (Process.res a p) (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} : lts.HomBisimilarity p q → lts.HomBisimilarity (p.choice r) (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} : lts.HomBisimilarity p q → lts.HomBisimilarity (p.par r) (q.par r)

P Q → P | R Q | R

theorem Cslib.CCS.bisimilarity_is_congruence {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} (p q : Process Name Constant) (c : Context Name Constant) (h : lts.HomBisimilarity p q) : lts.HomBisimilarity (c.fill p) (c.fill q)

Bisimilarity is a congruence in CCS.

instance Cslib.CCS.bisimilarityCongruence {Name : Type u} {Constant : Type v} {defs : Constant → Process Name Constant → Prop} : Congruence (Process Name Constant) lts.HomBisimilarity

Bisimilarity is a congruence in CCS.