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.

def Cslib.LTS.traces {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s : State) : Set (List Label)

The traces of a state s is the set of all lists of labels μs such that there is a multi-step transition labelled by μs originating from s.

Equations

• lts.traces s = {μs : List Label | ∃ (s' : State), lts.MTr s μs s'}

theorem Cslib.LTS.mem_traces_iff {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (μs : List Label) : μs ∈ lts.traces s ↔ ∃ (s' : State), lts.MTr s μs s'

Definition of LTS.traces for general label sequences, ...

theorem Cslib.LTS.mem_traces_singleton_iff {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (μ : Label) : [μ] ∈ lts.traces s ↔ ∃ (s' : State), lts.Tr s μ s'

... singleton sequences, ...

theorem Cslib.LTS.mem_traces_cons_iff {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (μ : Label) (μs : List Label) : μ :: μs ∈ lts.traces s ↔ ∃ (s' : State), lts.Tr s μ s' ∧ μs ∈ lts.traces s'

... and sequences extended with a single transition.

theorem Cslib.LTS.traces_in {State : Type u_1} {Label : Type u_2} {s : State} {μs : List Label} {s' : State} {lts : LTS State Label} (h : lts.MTr s μs s') : μs ∈ lts.traces s

If there is a multi-step transition from s labelled by μs, then μs is in the traces of s.

theorem Cslib.LTS.Deterministic.traces_of_tr {State : Type u_1} {Label : Type u_2} {s : State} {μ : Label} {s' : State} {lts : LTS State Label} [lts.Deterministic] (h : lts.Tr s μ s') : lts.traces s' = {μs : List Label | μ :: μs ∈ lts.traces s}

In a deterministic lts, a state's traces are determined by any of its predecessors.

theorem Cslib.LTS.Deterministic.traces_of_mTr {State : Type u_1} {Label : Type u_2} {s : State} {μs : List Label} {s' : State} {lts : LTS State Label} [lts.Deterministic] (h : lts.MTr s μs s') : lts.traces s' = {μs' : List Label | μs ++ μs' ∈ lts.traces s}

In a deterministic lts, a state's traces are determined by any of its multi-step predecessors.

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₂) : lts₁.traces s₁ ⊆ lts₂.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₂ = (lts₁.traces s₁ = 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.

@[implicit_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 mimiced 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 mimiced 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 preseved 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.