Event-structure semantics of CCS, and its coincidence with the operational one

@[reducible]

def CCS.empty {Name : Type u_2} : SES (Action Name)

No events.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def CCS.pfx {Name : Type u_2} (α : Action Name) (E : SES (Action Name)) : SES (Action Name)

Prefix α.E: a new event below everything, which every E-event needs.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def CCS.sum {Name : Type u_2} (E : SES (Action Name)) (F : SES (Action Name)) : SES (Action Name)

Sum E + F: disjoint events, and no configuration mixes the two sides.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def CCS.restrict {Name : Type u_2} (E : SES (Action (Option Name))) : SES (Action Name)

Restriction (ν)E: keep the visible events. An event is enabled only when some fully visible enabling set is available.

Equations

• One or more equations did not get rendered due to their size.

Projections of configurations

Each construction projects to its components, and the projection of a configuration is a configuration.

theorem CCS.pmapSet_pfx {Name : Type u_2} {E : SES (Action Name)} {α : Action Name} (s : Set (Option E.Event)) : GES.pmapSet id s = {z : E.Event | some z ∈ s}

theorem CCS.pmapSet_inl {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} (s : Set (E.Event ⊕ F.Event)) : GES.pmapSet Sum.getLeft? s = {z : E.Event | Sum.inl z ∈ s}

theorem CCS.pmapSet_inr {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} (s : Set (E.Event ⊕ F.Event)) : GES.pmapSet Sum.getRight? s = {z : F.Event | Sum.inr z ∈ s}

theorem CCS.pfx_con {Name : Type u_2} {E : SES (Action Name)} {α : Action Name} {c : Set (Option E.Event)} (h : (pfx α E).Consistent c) : E.Consistent {z : E.Event | some z ∈ c}

theorem CCS.pfx_isConf {Name : Type u_2} {E : SES (Action Name)} {α : Action Name} {c : Set (Option E.Event)} (hc : (pfx α E).isConf c) : E.isConf {z : E.Event | some z ∈ c}

The E-part of a configuration of α.E is a configuration.

theorem CCS.pfx_none_mem {Name : Type u_2} {E : SES (Action Name)} {α : Action Name} {c : Set (Option E.Event)} (hc : (pfx α E).isConf c) {z : E.Event} (hz : some z ∈ c) : none ∈ c

Every other event of a configuration of α.E requires the prefix.

theorem CCS.sum_con_L {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} (h : (sum E F).Consistent c) : E.Consistent {z : E.Event | Sum.inl z ∈ c}

theorem CCS.sum_con_R {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} (h : (sum E F).Consistent c) : F.Consistent {z : F.Event | Sum.inr z ∈ c}

theorem CCS.sum_isConf_L {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} (hc : (sum E F).isConf c) : E.isConf {z : E.Event | Sum.inl z ∈ c}

The E-part of a configuration of E + F is a configuration.

theorem CCS.sum_isConf_R {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} (hc : (sum E F).isConf c) : F.isConf {z : F.Event | Sum.inr z ∈ c}

The F-part of a configuration of E + F is a configuration.

theorem CCS.sum_not_mixed {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} (hc : (sum E F).isConf c) {z : E.Event} (hz : Sum.inl z ∈ c) {w : F.Event} (hw : Sum.inr w ∈ c) : False

A configuration of E + F never mixes the two sides.

theorem CCS.restrict_con {Name : Type u_2} {E : SES (Action (Option Name))} {c : Set (restrict E).Event} (h : (restrict E).Consistent c) : E.Consistent {y : E.Event | ∃ (hy : (E.label y).strip.isSome = true), ⟨y, hy⟩ ∈ c}

theorem CCS.pmapSet_unres {Name : Type u_2} {E : SES (Action (Option Name))} (s : Set (restrict E).Event) : GES.pmapSet (fun (e : (restrict E).Event) => some ↑e) s = {y : E.Event | ∃ (hy : (E.label y).strip.isSome = true), ⟨y, hy⟩ ∈ s}

theorem CCS.restrict_isConf {Name : Type u_2} {E : SES (Action (Option Name))} {c : Set (restrict E).Event} (hc : (restrict E).isConf c) : E.isConf {y : E.Event | ∃ (hy : (E.label y).strip.isSome = true), ⟨y, hy⟩ ∈ c}

The E-part of a configuration of (ν)E is a configuration.

Extending a configuration

theorem CCS.someInv_insert {Name : Type u_2} {E : SES (Action Name)} {c : Set (Option E.Event)} {x : E.Event} : {z : E.Event | some z ∈ c ∪ {some x}} = {z : E.Event | some z ∈ c} ∪ {x}

theorem CCS.pfx_isConf_insert {Name : Type u_2} {E : SES (Action Name)} {α : Action Name} {c : Set (Option E.Event)} {x : E.Event} (hc : (pfx α E).isConf c) (hnone : none ∈ c) (hx : E.isConf ({z : E.Event | some z ∈ c} ∪ {x})) (_hfr : some x ∉ c) : (pfx α E).isConf (c ∪ {some x})

theorem CCS.inlInv_insert {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} {x : E.Event} : {z : E.Event | Sum.inl z ∈ c ∪ {Sum.inl x}} = {z : E.Event | Sum.inl z ∈ c} ∪ {x}

theorem CCS.inrInv_insert {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} {y : F.Event} : {z : F.Event | Sum.inr z ∈ c ∪ {Sum.inr y}} = {z : F.Event | Sum.inr z ∈ c} ∪ {y}

theorem CCS.sum_isConf_insert_L {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} {x : E.Event} (hc : (sum E F).isConf c) (hnoR : ¬∃ (f : F.Event), Sum.inr f ∈ c) (hx : E.isConf ({z : E.Event | Sum.inl z ∈ c} ∪ {x})) : (sum E F).isConf (c ∪ {Sum.inl x})

theorem CCS.sum_isConf_insert_R {Name : Type u_2} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (E.Event ⊕ F.Event)} {y : F.Event} (hc : (sum E F).isConf c) (hnoL : ¬∃ (e : E.Event), Sum.inl e ∈ c) (hy : F.isConf ({z : F.Event | Sum.inr z ∈ c} ∪ {y})) : (sum E F).isConf (c ∪ {Sum.inr y})

theorem CCS.restrict_isConf_insert {Name : Type u_2} {E : SES (Action (Option Name))} {c : Set (restrict E).Event} {x : E.Event} {hx : (E.label x).strip.isSome = true} (hc : (restrict E).isConf c) (hxc : E.isConf ({y : E.Event | ∃ (hy : (E.label y).strip.isSome = true), ⟨y, hy⟩ ∈ c} ∪ {x})) : (restrict E).isConf (c ∪ {⟨x, hx⟩})

def CCS.unres {Name : Type u_2} {E : SES (Action (Option Name))} (c : Set (restrict E).Event) : Set E.Event

A configuration of (ν)E seen in E.

Equations

• CCS.unres c = {y : E.Event | ∃ (h : (E.label y).strip.isSome = true), ⟨y, h⟩ ∈ c}

theorem CCS.mem_unres {Name : Type u_2} {E : SES (Action (Option Name))} {c : Set (restrict E).Event} {x : E.Event} (hx : (E.label x).strip.isSome = true) : x ∈ unres c ↔ ⟨x, hx⟩ ∈ c

theorem CCS.unres_eq_image {Name : Type u_2} {E : SES (Action (Option Name))} {c : Set (restrict E).Event} : unres c = Subtype.val '' c

theorem CCS.unres_finite {Name : Type u_2} {E : SES (Action (Option Name))} {c : Set (restrict E).Event} (h : c.Finite) : (unres c).Finite

theorem CCS.unres_insert {Name : Type u_2} {E : SES (Action (Option Name))} {c : Set (restrict E).Event} {x : E.Event} (hx : (E.label x).strip.isSome = true) : unres (c ∪ {⟨x, hx⟩}) = unres c ∪ {x}

@[reducible]

def CCS.semantics {Name : Type u} : Process Name → SES (Action Name)

Event-structure semantics of finitary CCS, as stable event structures.

Equations

• CCS.semantics CCS.Process.nil = CCS.empty
• CCS.semantics (CCS.Process.pre α P) = CCS.pfx α (CCS.semantics P)
• CCS.semantics (P.sum Q) = CCS.sum (CCS.semantics P) (CCS.semantics Q)
• CCS.semantics (P.par Q) = CCS.parSES (CCS.semantics P) (CCS.semantics Q)
• CCS.semantics P.res = CCS.restrict (CCS.semantics P)

def CCS.opLTSI {Name : Type u_2} (P : Process Name) : LTSI (Action Name)

Operational LTSI from CCS step relation (no independence).

Equations

• One or more equations did not get rendered due to their size.

def CCS.denLTSI {Name : Type u_2} (P : Process Name) : LTSI (Action Name)

Denotational LTSI: configurations of the semantics.

Equations

• CCS.denLTSI P = (CCS.semantics P).toFamily.toLTSI