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).
• TraceEq.deterministic_sim: 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.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.

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.

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.deterministic_isSimulation {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.