The LTSI of a prime event structure

def PES.emptyConfig {L : Type u_1} (es : PES L) : Conf es

The empty configuration.

Equations

• es.emptyConfig = ⟨∅, ⋯⟩

def PES.esStep {L : Type u_1} (es : PES L) (c₁ : Conf es) (a : L) (c₂ : Conf es) : Prop

Forward step: extend by a fresh enabled event.

Equations

• es.esStep c₁ a c₂ = ∃ (e : es.Event), Configuration.enables es (↑c₁) e ∧ e ∉ ↑c₁ ∧ es.label e = a ∧ ↑c₂ = ↑c₁ ∪ {e}

def PES.esIndep {L : Type u_1} (es : PES L) (c : Conf es) (a : L) (c₁ : Conf es) (b : L) (c₂ : Conf es) : Prop

Coinitial independence: concurrent fresh enabled events.

Equations

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

def PES.toLTSI {L : Type u_1} (es : PES L) : LTSI L

LTSI of an event structure.

Equations

• es.toLTSI = { State := Conf es, init := es.emptyConfig, step := es.esStep, indep := es.esIndep }

theorem PES.esStep_iff {L : Type u_1} (es : PES L) {c₁ c₂ : Conf es} {a : L} : es.toFamily.esStep c₁ a c₂ ↔ es.esStep c₁ a c₂

The prime and family step relations agree.

theorem PES.esIndep_iff {L : Type u_1} (es : PES L) {c c₁ c₂ : Conf es} {a b : L} : es.toFamily.esIndep c a c₁ b c₂ ↔ es.esIndep c a c₁ b c₂

The prime and family independence relations agree.

theorem PES.toLTSI_eq {L : Type u_1} (es : PES L) : es.toLTSI = es.toFamily.toLTSI

The prime LTSI is the family LTSI.

theorem PES.toLTSI_LPV {L : Type u_1} (es : PES L) : es.toLTSI.LPV

The event-structure LTSI satisfies LPV.

def PES.esRStep {L : Type u_1} (es : PES L) : Conf es → DirLabel L → Conf es → Prop

Reversible step.

Equations

• es.esRStep = es.toFamily.esRStep

def PES.esRIndep {L : Type u_1} (es : PES L) : Conf es → DirLabel L → Conf es → DirLabel L → Conf es → Prop

Reversible coinitial independence.

Equations

• es.esRIndep = es.toFamily.esRIndep

def PES.toRLTSI {L : Type u_1} (es : PES L) : RLTSI L

Reversible LTSI of an event structure.

Equations

• es.toRLTSI = es.toFamily.toRLTSI

theorem PES.toRLTSI_LPV {L : Type u_1} (es : PES L) : es.toRLTSI.LPV

Prime event structures are stable, so the reverse LPV axioms hold.