Trace Equivalence

Definitions and results on trace equivalence for LTSs.

Main definitions

• LTS.traces: the set of traces of a state.
• TraceEq s₁ s₂: s₁ and s₂ are trace equivalent, i.e., they have the same sets of traces.

Notations

• s₁ ~tr[lts] s₂: the states s₁ and s₂ are trace equivalent in lts.

Main statements

• TraceEq.eqv: trace equivalence is an equivalence relation (see Equivalence).
• Deterministic.isSimulation_traceEq: in any deterministic LTS, trace equivalence is a simulation.

theorem Cslib.LTS.IsSimulation.traces_subset {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} {s₁ : State✝} {s₂ : State✝¹} (hr : lts₁.IsSimulation lts₂ r) (hrel : r s₁ s₂) : traces s₁ ⊆ traces s₂

If s₁ is simulated by s₂ all of s₁'s traces are also traces of s₂.

def Cslib.LTS.TraceEq {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (s₁ : State₁) (s₂ : State₂) : Prop

Two states are trace equivalent if they have the same set of traces.

Equations

• lts₁.TraceEq lts₂ s₁ s₂ = (Cslib.LTS.traces s₁ = Cslib.LTS.traces s₂)

def Cslib.LTS.«term_~tr[_,_]_» : Lean.TrailingParserDescr

Notation for trace equivalence.

Differently from standard pen-and-paper presentations, we require the LTSs to be mentioned explicitly.

Equations

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

@[reducible, inline]

abbrev Cslib.LTS.HomTraceEq {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s₁ s₂ : State) : Prop

Homogeneous trace equivalence compares states on the same LTS.

Equations

• lts.HomTraceEq = lts.TraceEq lts

def Cslib.LTS.«term_~tr[_]_» : Lean.TrailingParserDescr

Notation for homogeneous trace equivalence.

Equations

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

theorem Cslib.LTS.HomTraceEq.refl {State : Type u_1} {Label✝ : Type u_2} {lts : LTS State Label✝} (s : State) : lts.HomTraceEq s s

Homogeneous trace equivalence is reflexive.

@[simp]

theorem Cslib.LTS.TraceEq.flip_eq {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : flip (lts₁.TraceEq lts₂) = lts₂.TraceEq lts₁

theorem Cslib.LTS.TraceEq.symm {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {s₁ : State✝} {s₂ : State✝¹} (h : lts₁.TraceEq lts₂ s₁ s₂) : lts₂.TraceEq lts₁ s₂ s₁

Trace equivalence is symmetric.

theorem Cslib.LTS.TraceEq.trans {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {s₁ : State✝} {s₂ : State✝¹} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} {s₃ : State✝²} (h1 : lts₁.TraceEq lts₂ s₁ s₂) (h2 : lts₂.TraceEq lts₃ s₂ s₃) : lts₁.TraceEq lts₃ s₁ s₃

Trace equivalence is transitive.

theorem Cslib.LTS.HomTraceEq.eqv {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} : Equivalence fun (x1 x2 : State✝) => lts.HomTraceEq x1 x2

Homogeneous trace equivalence is an equivalence relation.

@[instance_reducible]

instance Cslib.LTS.instTransTraceEq {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} : Trans (lts₁.TraceEq lts₂) (lts₂.TraceEq lts₃) (lts₁.TraceEq lts₃)

calc support for simulation equivalence.

Equations

• Cslib.LTS.instTransTraceEq = { trans := ⋯ }

theorem Cslib.LTS.TraceEq.exists_mTr_of_mTr {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {s₁ : State₁} {s₂ : State₂} {μs : List Label} {s₁' : State₁} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} (h : lts₁.TraceEq lts₂ s₁ s₂) (htr : lts₁.MTr s₁ μs s₁') : ∃ (s₂' : State₂), lts₂.MTr s₂ μs s₂'

For trace-equivalent states, any multistep transition of one can be mimicked by the other.

theorem Cslib.LTS.TraceEq.exists_tr_of_tr {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {s₁ : State₁} {s₂ : State₂} {μ : Label} {s₁' : State₁} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} (h : lts₁.TraceEq lts₂ s₁ s₂) (htr : lts₁.Tr s₁ μ s₁') : ∃ (s₂' : State₂), lts₂.Tr s₂ μ s₂'

For trace-equivalent states, any single-step transition of one can be mimicked by the other.

theorem Cslib.LTS.TraceEq.traceEq_of_tr_of_tr {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {s₁ : State₁} {s₂ : State₂} {μ : Label} {s₁' : State₁} {s₂' : State₂} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [hdet₁ : lts₁.Deterministic] [hdet₂ : lts₂.Deterministic] (h : lts₁.TraceEq lts₂ s₁ s₂) (htr₁ : lts₁.Tr s₁ μ s₁') (htr₂ : lts₂.Tr s₂ μ s₂') : lts₁.TraceEq lts₂ s₁' s₂'

For deterministic lts's, trace equivalence is preserved by respective transitions with the same label.

theorem Cslib.LTS.Deterministic.isSimulation_traceEq {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [hdet₁ : lts₁.Deterministic] [hdet₂ : lts₂.Deterministic] : lts₁.IsSimulation lts₂ (lts₁.TraceEq lts₂)

In deterministic LTSs, trace equivalence is a simulation.

theorem Cslib.LTS.SimulationEquiv.traceEq {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {s₁ : State✝} {s₂ : State✝¹} (h : lts₁.SimulationEquiv lts₂ s₁ s₂) : lts₁.TraceEq lts₂ s₁ s₂

Simulation equivalence implies trace equivalence.

theorem Cslib.LTS.Deterministic.traceEq_iff_simulationEquiv {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [hdet₁ : lts₁.Deterministic] [hdet₂ : lts₂.Deterministic] (s₁ : State₁) (s₂ : State₂) : lts₁.TraceEq lts₂ s₁ s₂ ↔ lts₁.SimulationEquiv lts₂ s₁ s₂

Simulation equivalence and trace equivalence are equivalence for detemrinistic lts's.