Coincidence of the operational and denotational semantics of CCS

The bisimulation relates a configuration c of ⟦P⟧ to the residual process resid P c, computed structurally.

noncomputable def CCS.resid {Name : Type u} (P : Process Name) : Set (semantics P).Event → Process Name

The process remaining after a configuration has fired.

Equations

• One or more equations did not get rendered due to their size.
• CCS.resid CCS.Process.nil x_4 = CCS.Process.nil
• CCS.resid (CCS.Process.pre α P) c = if none ∈ c then CCS.resid P {e : (CCS.semantics P).Event | some e ∈ c} else CCS.Process.pre α P
• CCS.resid (P.par Q) c = (CCS.resid P (CCS.projL c)).par (CCS.resid Q (CCS.projR c))
• CCS.resid P.res c = (CCS.resid P (CCS.unres c)).res

@[simp]

theorem CCS.resid_nil {Name : Type u} (c : Set (semantics Process.nil).Event) : resid Process.nil c = Process.nil

theorem CCS.resid_pre_pos {Name : Type u} {α : Action Name} {P : Process Name} {c : Set (semantics (Process.pre α P)).Event} (h : none ∈ c) : resid (Process.pre α P) c = resid P {e : (semantics P).Event | some e ∈ c}

theorem CCS.resid_pre_neg {Name : Type u} {α : Action Name} {P : Process Name} {c : Set (semantics (Process.pre α P)).Event} (h : none ∉ c) : resid (Process.pre α P) c = Process.pre α P

theorem CCS.resid_sum_l {Name : Type u} {P Q : Process Name} {c : Set (semantics (P.sum Q)).Event} (h : ∃ (e : (semantics P).Event), Sum.inl e ∈ c) : resid (P.sum Q) c = resid P {e : (semantics P).Event | Sum.inl e ∈ c}

theorem CCS.resid_sum_r {Name : Type u} {P Q : Process Name} {c : Set (semantics (P.sum Q)).Event} (h1 : ¬∃ (e : (semantics P).Event), Sum.inl e ∈ c) (h2 : ∃ (f : (semantics Q).Event), Sum.inr f ∈ c) : resid (P.sum Q) c = resid Q {f : (semantics Q).Event | Sum.inr f ∈ c}

theorem CCS.resid_sum_none {Name : Type u} {P Q : Process Name} {c : Set (semantics (P.sum Q)).Event} (h1 : ¬∃ (e : (semantics P).Event), Sum.inl e ∈ c) (h2 : ¬∃ (f : (semantics Q).Event), Sum.inr f ∈ c) : resid (P.sum Q) c = P.sum Q

theorem CCS.resid_par {Name : Type u} {P Q : Process Name} (c : Set (semantics (P.par Q)).Event) : resid (P.par Q) c = (resid P (projL c)).par (resid Q (projR c))

theorem CCS.resid_res {Name : Type u} {P : Process (Option Name)} (c : Set (semantics P.res).Event) : resid P.res c = (resid P (unres c)).res

@[simp]

theorem CCS.resid_empty {Name : Type u} (P : Process Name) : resid P ∅ = P

theorem CCS.den_to_op {Name : Type u} (P : Process Name) (c : Set (semantics P).Event) (e : (semantics P).Event) : (semantics P).isConf c → (semantics P).isConf (c ∪ {e}) → e ∉ c → Step (resid P c) ((semantics P).label e) (resid P (c ∪ {e}))

Completeness: firing an enabled event is a step of the residual process.

theorem CCS.op_to_den {Name : Type u} (P : Process Name) (c : Set (semantics P).Event) (α : Action Name) (Q' : Process Name) : (semantics P).isConf c → Step (resid P c) α Q' → ∃ (e : (semantics P).Event), (semantics P).isConf (c ∪ {e}) ∧ e ∉ c ∧ (semantics P).label e = α ∧ Q' = resid P (c ∪ {e})

Soundness: every step of the residual process fires an enabled event.

theorem CCS.op_den_bisim {Name : Type u} (P : Process Name) : Bisimilar (opLTSI P) (denLTSI P)

Coincidence of the two semantics, via the residual process.